2004-10-11 berghofe 2004-10-11 Added entry in Settings menu for Toplevel.skip_proofs flag.
2004-10-11 berghofe 2004-10-11 Some changes to allow skipping of proof scripts.
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-10-11 nipkow 2004-10-11 Induction now preserves the name of the induction variable.
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
2004-10-06 chaieb 2004-10-06 *** empty log message ***
2004-10-06 chaieb 2004-10-06 a very simple decision procedure for a fragment of bounded arithmetic
2004-10-06 chaieb 2004-10-06 changed in order to insert Barith.thy
2004-10-05 paulson 2004-10-05 auto update
2004-10-05 paulson 2004-10-05 new simprules for abs and for things like a/b<1
2004-10-04 paulson 2004-10-04 revised simprules for division
2004-10-04 paulson 2004-10-04 PDF_VIEWER suggestion
2004-10-04 paulson 2004-10-04 Abstract for the Isabelle system
2004-10-02 aspinall 2004-10-02 Add openblock/closeblock to other opengoal/closegoal elements
2004-10-01 aspinall 2004-10-01 Allow scanning to recover and reconstruct bad input
2004-10-01 paulson 2004-10-01 patch to "display"
2004-10-01 paulson 2004-10-01 display-drafts now uses pdf!
2004-10-01 paulson 2004-10-01 tweaking of arithmetic proofs
2004-10-01 aspinall 2004-10-01 Comments
2004-09-30 paulson 2004-09-30 tidied
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