2004-09-03 obua 2004-09-03 Matrix theory, linear programming
2004-09-03 paulson 2004-09-03 new theorem symD
2004-09-03 paulson 2004-09-03 listrel operator for lifting relations to lists
2004-09-03 aspinall 2004-09-03 Fix file:/// and file://localhost/ to give absolute paths
2004-09-03 aspinall 2004-09-03 Fix file:/// and file://localhost/ to return local file result
2004-09-03 aspinall 2004-09-03 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
2004-09-02 paulson 2004-09-02 new example of a quotiented nested data type
2004-09-02 dixon 2004-09-02 added code to make use of case splitting to prove the specification equations for recursive definitions.
2004-09-02 paulson 2004-09-02 fixed presentation
2004-09-01 paulson 2004-09-01 new "respects" syntax for quotienting
2004-09-01 paulson 2004-09-01 new functions for sets of lists
2004-08-30 webertj 2004-08-30 reference to cla.ML replaced by Classical.thy
2004-08-30 chaieb 2004-08-30 commentar eliminated a line 156 - arith raised Match exception at m dvd 2
2004-08-30 chaieb 2004-08-30 corrected
2004-08-30 chaieb 2004-08-30 m dvd t where m is non numeral is now catched!
2004-08-29 webertj 2004-08-29 Provers/blast.ML: depth_limit
2004-08-29 webertj 2004-08-29 depth limit (previously hard-coded with a value of 20) made a reference
2004-08-26 webertj 2004-08-26 comment modified
2004-08-24 obua 2004-08-24 changes
2004-08-23 berghofe 2004-08-23 begin_theory now takes optional path (current directory) as argument. This is needed for locating *.ML files connected with theories.
2004-08-23 berghofe 2004-08-23 Fixed several bugs related to path specifications in theory names.
2004-08-23 berghofe 2004-08-23 Function check_file now takes optional path (current directory) as an argument.
2004-08-23 berghofe 2004-08-23 Adapted to new interface of function ThyLoad.check_file
2004-08-23 berghofe 2004-08-23 Added function for "normalizing" absolute paths (i.e. dereferencing of symbolic links; the functions in path.ML cannot do this). This is used by function full_path.
2004-08-23 webertj 2004-08-23 new isatool dimacs2hol
2004-08-23 webertj 2004-08-23 initial version
2004-08-20 paulson 2004-08-20 new examples
2004-08-20 paulson 2004-08-20 proof reconstruction for external ATPs
2004-08-20 paulson 2004-08-20 fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
2004-08-19 nipkow 2004-08-19 new import syntax
2004-08-19 nipkow 2004-08-19 *** empty log message ***
2004-08-19 aspinall 2004-08-19 Add systemcmd.
2004-08-19 aspinall 2004-08-19 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
2004-08-18 aspinall 2004-08-18 Version for PGIP 2.X, with greatly improved parsing and XML handling.
2004-08-18 aspinall 2004-08-18 Remove isar_readstring. Split read into scanner and parser.
2004-08-18 aspinall 2004-08-18 Make token an eqtype to assist reconstructing input
2004-08-18 aspinall 2004-08-18 Add scan_comment_whspc to skip space and comments in PGIP stream
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-17 kleing 2004-08-17 todo before next release
2004-08-17 kleing 2004-08-17 improved wording course material
2004-08-17 kleing 2004-08-17 include course material page
2004-08-16 nipkow 2004-08-16 Adapted text to new theory header syntax.
2004-08-16 nipkow 2004-08-16 Added "import" and "begin"
2004-08-16 aspinall 2004-08-16 Experimental version supporting PGIP, merged with main branch with help from Makarius.
2004-08-16 aspinall 2004-08-16 Experimental pgip_isar.xml file
2004-08-16 nipkow 2004-08-16 new theory header syntax.
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-16 nipkow 2004-08-16 *** empty log message ***
2004-08-16 berghofe 2004-08-16 Replaced `div and `mod in consts_code section by div and mod.
2004-08-14 webertj 2004-08-14 bugfix in read_dimacs_cnf_file
2004-08-12 ballarin 2004-08-12 Disallowed "includes" in locale declarations.
2004-08-10 berghofe 2004-08-10 Fixed bug in compile_clause that caused equality constraints to be "forgotten".
2004-08-09 webertj 2004-08-09 warning for recursion over IDTs added
2004-08-09 nipkow 2004-08-09 Aded a thm.
2004-08-06 chaieb 2004-08-06 *** empty log message ***
2004-08-06 chaieb 2004-08-06 proof_of_evalc corrected;
2004-08-06 nipkow 2004-08-06 Initial changes to extend arithmetic from individual types to type classes.
2004-08-06 nipkow 2004-08-06 undid UN/INT syntax
2004-08-06 nipkow 2004-08-06 undid UN/INT xsymbol syntax with subscripts.