o Fixed bug in reduction mechanism which stopped reduction of non-strict (but case!)
  function arguments.
  Also fixed several minor other bugs in reduction.
o Lowered the maximum reduction cap to 500 steps.
o Introduced maximum display depth for showing expressions.
o Allowed reduction to normal form to continue through let variables.
  Added manual let lifting and garbage collection to reduction to NF.
  Changed normal reduction to perform garbage collection immediately in the following two cases:
  - reduction of a lazy let;
  - creation of lets for the purpose of unsharing a rnf.

-------------------------------------------------------------------------------------------
Version 1.0a (3 July 2008)
-------------------------------------------------------------------------------------------
o Interpreter back operational.
o Reduction mechanism now maintains lets within expressions, and performs let lifting and
  let joining when necessary. Garbage collection is also performed automatically by
  reduction, and costs one step for each variable removed.
o Added tactic: MakeUnique (still buggy).
o Added tactic: ManualDefinedness.
o Added tactic: Unshare.

-------------------------------------------------------------------------------------------
Version 0.0.5e (April 2008)
-------------------------------------------------------------------------------------------
o WARNING: The interpreter is STILL not operational!
o Fixed: when an error occurs, focus is now correctly set on the commandline.
o Added menu option (with quick-key Ctrl-C) to force focus on the commandline.
o Fixed typing algorithm; String should now correctly unify with {#Char}.
o Implicit Cases is no longer allowed on expressions that do not occur in the current
  goal.
o Added a warning dialog that is displayed when modules from the normal StdEnv have
  been loaded into memory.
o Contradiction on a hypothesis is no longer generated as hint if the resulting goal
  will be equal to the starting one.
o Removed 'saved changed sections' from the 'Theorems' menu.
o Changed admissability analysis. Sign is no longer flipped for existential quantors.

-------------------------------------------------------------------------------------------
Version 0.0.5d (20 June 2007)
-------------------------------------------------------------------------------------------
o WARNING: The interpreter is STILL not operational!
o Due to buggy behavior, access to the tactics ExpandFun, MoveInCase and RemoveCase has
  temporarily been removed.

-------------------------------------------------------------------------------------------
Version 0.0.5c (20 September 2006)
-------------------------------------------------------------------------------------------
o WARNING: The interpreter is STILL not operational!
o Admissability analysis widened.
  Case (e1 = e2) : negative now succeeds if the variable is not used in e1 nor e2.
  FORALL e.p                now recursively continues on p (instead of failing).
  EXISTS e.p                now recursively (flipped) continues on p (instead of failing).
o Added the possibility to temporary (within one run of Sparkle) fold proof nodes.
  Added buttons 'fold inactive' and 'unfold all' to TheoremWindow.
o Definedness analysis now stores original statement as well.
  For example: if H1 = ~(i + 1) = _|_,
               then the expressions i and (i+1) are both marked as defined.
  Previously, decomposition caused only i to be marked as defined.
o Added support for 'MatchExpr' alternative.
  Left-hand patterns in lets and wheres should work now.

-------------------------------------------------------------------------------------------
Version 0.0.5b (22 June 2006)
-------------------------------------------------------------------------------------------
o Rewrote reduction function. Same functionality, several minor bugs in relation to
  the reduction of functions with strict arguments have been corrected.
  WARNING: Due to these changes, the interpreter is not operational any more!
o Rewrote check for case-variables. Now only produces variables on which a case
  distinction is always performed.
o A non-strict case variable is now treated as if it was strict.
o The 'restart' button on the theorem window is now always applicable, even if the
  theorem is used elsewhere. (the 'go' button on the restart-window now does this check)

-------------------------------------------------------------------------------------------
Version 0.0.4a (03 October 2003)
-------------------------------------------------------------------------------------------
o Updated to a later version of the compiler. Due to some internal changes in the compiler,
  this has the side-effect that some proof sections that were constructed using Sparkle 0.0.3a
  will no longer load correctly in Sparkle 0.0.4a. The following sections are affected:
  
  - All sections that depend on a dictionary, which is most likely to be the case if a
    dictionary is created for a top-level theorem in the section.
    
  The change within the compiler can be summarized as follows: a semi-colon is added to
  the name of each dictionary type. This also affects the names of the functions that
  create a dictionary, select fields from a dictionary and update a dictionary.
  
  The error message that is displayed when an attempt is made to load the section anyway
  will always be of the form:
  
  - "Unable to find symbol X of type Y", where either in X or in Y a reference to a
    dictionary is made.
    
  Unfortunately, this problem can only be corrected by manually editing the section files,
  which are stored in the /Sections subdirectory. Each file begins with a list of SECTION
  DEPENDENCIES. Within this list, the following changes have to be made:
  
  - [dictionary_types]
    All references to "dictionary_<class name>" must be replaced with
                      "dictionary_<class name>;".
  - [dictionary creation]
    All references to "_create_dictionary_<class name>" must be replaced with
                      "_create_dictionary_<class name>;".
  - [dictionary selection]
    All references to "_dictionary_<class name>_select_<member name>" must be replaced with
                      "_dictionary_<class name>;_select_<member name>".
  - [dictionary update]
    All references to "_dictionary_<class name>_updatet_<member name>" must be replaced with
                      "_dictionary_<class name>;_update_<member name>".

-------------------------------------------------------------------------------------------
Version 0.0.3a (21 February 2003)
-------------------------------------------------------------------------------------------
o Relaxed constraints on 'Injective'.
  Now also applicable when applied on a constructor application in a hypothesis which
  is known to be defined.

-------------------------------------------------------------------------------------------
Version 0.0.3a (21 January 2002)
-------------------------------------------------------------------------------------------

o Fixed bug in typing algorithm, causing problems with typing variables in goals.
  The erronous situation occurred for example when one hypothesis produced 'x :: a -> Bool'
  and another one produced 'x :: Int -> b'. A unification error used to be given here.
o Fixed bug in mechanism to propagate defaults in cases.
  Complicated patterns used to be handled incorrectly by Sparkle.
o Added feature: a case within the SAME case is now filled in by Sparkle.

-------------------------------------------------------------------------------------------
Version 0.0.3a (8 January 2002)
-------------------------------------------------------------------------------------------

o Fixed bug with finding Standard Sparkle Environment on some Windows 95/98
  machines. Bug was caused by function 'applicationpath' (from the Object I/O),
  which incorrectly returns the path in MSDOS format (8.3 and all uppercases) on
  some machines.
o Fixed bug with projects where the main module also has a .dcl module.
  These projects can now be loaded correctly.
o Renamed the module 'SparkleEnv' from the Standard Sparkle Environment to
  'StdSparkle'. Made 'StdEnv' again the top-level module (instead of 'SparkleEnv').
  It imports 'StdSparkle'.

-------------------------------------------------------------------------------------------
Version 0.0.2a (21 December 2001)
-------------------------------------------------------------------------------------------
