2004-09-11 nipkow 2004-09-11 undoing previous change
2004-09-11 nipkow 2004-09-11 antisymmetry simproc
2004-09-10 nipkow 2004-09-10 Added antisymmetry simproc
2004-09-10 obua 2004-09-10 IntInf.divMod replaced by IntInf.div, IntInt.mod
2004-09-10 nipkow 2004-09-10 new forward deduction capability for simplifier
2004-09-09 paulson 2004-09-09 new hooks for resolution by Jia Meng
2004-09-09 aspinall 2004-09-09 Fix for schema changes in pgiptype
2004-09-08 aspinall 2004-09-08 Tweak parentnames attribute on opentheory
2004-09-08 aspinall 2004-09-08 Support parsing of -- {* comments *}. Add extra output channels.
2004-09-08 aspinall 2004-09-08 Add info and debug output channels.
2004-09-08 obua 2004-09-08 Adapted FloatArith.ML to SMLNJ 10.0.7
2004-09-07 oheimb 2004-09-07 integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
2004-09-07 oheimb 2004-09-07 added check against indirect recursion
2004-09-07 nipkow 2004-09-07 fixed discrete field.
2004-09-07 nipkow 2004-09-07 tuned "discrete" field
2004-09-06 nipkow 2004-09-06 made mult_mono_thms generic.
2004-09-06 paulson 2004-09-06 now rejects degenerate (looping) cases
2004-09-06 paulson 2004-09-06 new "respects" syntax for the congruent operator
2004-09-03 nipkow 2004-09-03 *** empty log message ***
2004-09-03 obua 2004-09-03 float2real is now globally available
2004-09-03 obua 2004-09-03 Matrix theory
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