release-0.93

• send structured theories to the VSE prover
  • still experimental and
  • only for those that have VSE
• normal form computation
  • available for CASL and extensions (like VSE)
  • turned out to be too slow to be included in "automatic"
• logic OWL improved
• HasCASL to Isabelle translation improved
• ongoing work on other logics
  • CspCASL

release-0.9

• connection to the VSE prover
  • for single theories only
  • the VSE prover is currently non-free
• normal form computation (unoptimized) used within
  • proof rule: theoremHideShift
  • theories of most nodes
  • conservativity checks
• added flattening operation for globally coding out:
  • heterogeneity, hiding,
  • renaming, importing,
  • disjoint unions
• extended Isabelle comorphism
• creating heterogeneous proof scripts
• switched to GTK (requires more libraries)

release-0.87

• works with Isabelle 2008
• no frameworks needed for Macs
• logic VSE added
• OWL changes

release-0.85

• logic !RelScheme and a comorphism to CASL
• code refactoring regarding
  • GUI
  • development graph
  • its calculus
• additions to
  • logic CspCASL and DL
  • colimit computations

release-0.8

• Haskell and HasCASL to Isabelle encoding
• CASL colimit computation
• CspCASL parser
• OWL 1.1
• concurrent proofs
• support for extended signatures

release-0.75

• completed logic Propositional
• completed command line interface
• improved graphical user interface
• clarified many HasCASL features and fixed bugs
• improved the encoding from CASL to Isabelle

release-0.73

• fixed many HasCASL wibbles and provided more examples
• improved the encoding into logic SoftFOL (used for automatic theorem provers, e.g. SPASS, Vampire)
  by the generation of "argument restrictions" for predicates which carry some typing information
• imported theorems (that are available as axioms) are marked with "(Th)" in the proof management GUI

release-0-7

• home page at !http://www.informatik.uni-bremen.de/dfki-sks/hets
• parsing and static analysis of CASL, CASL extensions, and other logics
• a (new) variety of logic translations
• connection to the theorem provers Isabelle, SPASS, Vampire and to the webservice prover !MathServe
• use of induction in connection with automated first-order provers
• OMDoc import and export
• some sample specifications about metric spaces and spatial calculi in HasCASL
• a new and easy-to-use Java-based installer

release-0-65

• Version 0.65 is mainly a bug-fix release
• Further efforts have been put into the proof support and into command line interface (by Razvan Pascanu)
• There is also an experimental binary distribution for Macs on Intel using ghc-6.6

release-0-60

• Hendrik Iben's OMDoc utilities have been integrated
• Paolo Torrini has improved the Haskell to Isabelle translation. Simple modules (without imports) can be read and translated via hets now.
• Much work has been put into the proof support, i.e. the GUI and translations to SPASS and Isabelle
• The (current) Basic Libraries, the CASL User Manual specifications and other examples are consistent (according to SPASS with a time limit of about 7 minutes.).
• Bugs and inefficiencies regarding sublogcs have been removed.
• LaTeX printing has been partially refactored.