Version: 1.0.1

	- Fixed a bug in the atom definition support where it could happen
          that variable dependencies between the atom definition and formulae
          outside the definition are discarded.

	- Fixed a bug in the renaming module, where in some cases a renaming
	  with non-zero benefit was not performed.

Version: 1.0.2

	- Fixed inconsistencies between the DFG proof format description in 
	  dfgsyntax.ps and the actual implementation. Proof checking is more 
	  more liberal, because the empty clause needs not to have the highest
	  clause number.

Version: 1.0.3

	- Sharpend renaming; it now potentially produces fewer clauses.

Version: 1.0.4

	- Changed some clause generation functions such that sequentially
	  applying FLOTTER, SPASS and just applying SPASS result in the
	  very same clause sets.

	- Added the new tool dfg2dfg that supports transformations into
	  monadic clause classes and their further approximations.

Version: 1.0.5

	- Improved SPASS man pages: In particular, we added further detailed 
	  explanations of inference rule flags and soft typing flags.

	- Significantly improved modularity of the code by making the flagstore
	  object part of the proof search object; so there is no global flagstore
	  around anymore. These changes touched nearly all modules.

	- Changed certain clause generation procedures such that now applying SPASS
	  directly to a formula or subsequent application of FLOTTER and SPASS produce
	  exactly the same ordering of a clause set (literlas). Since the behaviour of
	  SPASS is not independant from initial clause/literal orderings the changes
	  make SPASS results a little more robust/more predictable.
	  As all code was touched, we also included a code style review (comments,
	  prototypes, ...).

	- Flag values given to SPASS are now checked and rejected if out of range.

Version: 1.0.6

	- Strengthened prototyping of functions in particular in the case of function
	  arguments. This resulted in specialized extra functions.
	  
	- Improved printing efficiency by replacing (f)printf calls with (f)puts calls
	  whenever possible.

	- Removed the modul global precedence variable of the symbol modul and replaced
	  it by argument passing. The precedence is now stored in the proofsearch structure.
	  This affected huge parts of the SPASS code.

	- Adjusted comments and code layout.

	- Strengthened warnings for the gcc compiler.

	- Increased usage of the string module.


Version: 2.0.0

	- Corrections to spellings, documentation.

	- Added handbooks for SPASS and dfg2dfg.

	- Added contextual rewriting.

	- Added semantic tautology check.

	- Fixed bugs in CNF translation: Renaming, Equation elimination rules.

	- Improved splitting clause selection on the basis of reduction potential.

	- Improved robustness of initial clause list ordering.

	- Added the terminator module.

	- Extended formula definition detection/expansion to so called guarded definitions.

	- Improved determination of initial precedence such that as many as possible
	  equations in the input clause list can be oriented.

	- Added mainloop without complete interreduction.

	- Developed PROOFSEARCH data type enabling a modularization of the SPASS
	  source code on search engine level, such that several proof attempts can
	  now be run completely independantly at the same time within SPASS.

	- Moved GUI to Qt 3.0. The GUI now also includes dfg2dfg and new even more
	  user friendly layout. The GUI runs on any platform where SPASS and Qt are
	  available.

Version: 2.1

	- Fixed a bug in the definition module. Formulae were not normalized before
	  application of the procedure, leading to wrong matchings of variables.

	- Fixed a bug in the flag module. The subproof flagstore settings were not
	  complete: ordering flag and the weight flags were missing.

	- Fixed a bug in dfgparser.y, where a missing semicolon with
	  bison version 1.75 now caused an error.

	- Fixed a bug in cnf.c where the formula "equiv(false,false)" was
	  not properly treated in function cnf_RemoveTrivialAtoms.

	- Fixed a bug in symbol_LowerSignature where capital 'A's and 'Z's were not
	  prefixed by a lowercase 'ss' due to their exclusion in the condition. This
	  caused problems in the result of dfg2tptp applied to dfg input files with
	  uppercase symbols starting with an 'A' or 'Z'.

	- Now dfg2otter negates conjecture formulae of the SPASS input file
	  before printing the Otter usable list.

	- Added man pages for dfg2ascii, dfg2otter and dfg2tptp.