Miscellaneous bug fixes, particularly for prover interfaces to SNARK and Isabelle/HOL.
We now use Steel Bank Common Lisp (SBCL) as the host system for Specware on Linux and Mac OS X. This improves Specware's speed and supports Specware for Mac OS X on Intel.
Miscellaneous bug fixes.
New language features (Specware Language Manual section in parentheses)
Guarded patterns (2.7.2)
Special syntax for monads (2.6.16)
Underscore (_) is a wild card in qualifications in translations (2.3.2.3)
Sum and Quotient types are only allowed at the top-level, i.e., on the right-hand side of type definitions (2.4.3)
New combined op and def syntax to facilitate sub-type definition (2.4.4). E.g.,
op [a] nth (l : List a, i : Nat | i < length l) : List a = ...
Allow switch between word and non-word style in names at underscore (2.2.1). E.g. , +_2
Hexadecimal literals (2.2.1)
Use of X-Symbol package to support non-ascii symbols (2.2.2)
Also see Chapter 9 of the Specware User manual.
New Libraries (under Library/General).
Experimental support for using Isabelle/HOL to prove proof obligations. See Specware-Isabelle Interface manual.