2004-09-30 kleing 2004-09-30 display pdf as well as dvi
2004-09-30 schirmer 2004-09-30 bug-fix with new records
2004-09-29 aspinall 2004-09-29 Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.
2004-09-29 schirmer 2004-09-29 tuned performance of record definition
2004-09-29 paulson 2004-09-29 tidying up; identifying the main theorems
2004-09-28 ballarin 2004-09-28 Changes in "includes".
2004-09-28 ballarin 2004-09-28 Bug fixes.
2004-09-28 aspinall 2004-09-28 Add text_charref to encode a string using character references
2004-09-28 aspinall 2004-09-28 Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
2004-09-28 aspinall 2004-09-28 Fix to unparse to not double-escape backslash
2004-09-27 aspinall 2004-09-27 Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
2004-09-27 aspinall 2004-09-27 Add newline after CDATA for sake of HaXml
2004-09-27 ballarin 2004-09-27 Modified locales: improved implementation of "includes".
2004-09-23 paulson 2004-09-23 some x-symbols
2004-09-23 berghofe 2004-09-23 - Inserted additional check for equality types in check_mode_clause that avoids ill-typed code to be generated. - Mode inference algorithm now outputs additional diagnostic messages.
2004-09-22 schirmer 2004-09-22 bug-fix
2004-09-19 paulson 2004-09-19 converting UNITY/MultisetSum.ML to Isar script
2004-09-17 paulson 2004-09-17 converted ZF/Induct/Multiset to Isar script
2004-09-13 nipkow 2004-09-13 *** empty log message ***
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.