2004-11-24 berghofe 2004-11-24 Added EfficientNat
2004-11-24 berghofe 2004-11-24 Code generator plug-in for implementing natural numbers by integers.
2004-11-24 berghofe 2004-11-24 Added Library/EfficientNat
2004-11-24 berghofe 2004-11-24 Reimplemented some operations on "code lemma" table to avoid that code lemmas get lost during merge.
2004-11-24 berghofe 2004-11-24 New theorem zpower_int
2004-11-24 nipkow 2004-11-24 *** empty log message ***
2004-11-23 obua 2004-11-23 prettier proof of setsum_diff
2004-11-23 webertj 2004-11-23 HTML conformity
2004-11-23 nipkow 2004-11-23 renamed 1 lemmas
2004-11-23 nipkow 2004-11-23 renamed 2 lemmas
2004-11-23 obua 2004-11-23 relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
2004-11-23 webertj 2004-11-23 external solvers may now overwrite existing temporary files
2004-11-23 nipkow 2004-11-23 added lemma
2004-11-23 obua 2004-11-23 Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
2004-11-23 nipkow 2004-11-23 *** empty log message ***
2004-11-23 nipkow 2004-11-23 generalized lemma
2004-11-23 nipkow 2004-11-23 added lemma
2004-11-22 paulson 2004-11-22 indentation
2004-11-22 nipkow 2004-11-22 fixed proof
2004-11-22 nipkow 2004-11-22 added lemmas
2004-11-21 nipkow 2004-11-21 Added more lemmas
2004-11-21 nipkow 2004-11-21 added lemmas
2004-11-21 nipkow 2004-11-21 Restructured List and added "rotate"
2004-11-19 webertj 2004-11-19 comment modified
2004-11-19 paulson 2004-11-19 moved and renamed Integ/Equiv.thy
2004-11-19 webertj 2004-11-19 solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
2004-11-19 chaieb 2004-11-19 Barith removed VS: ----------------------------------------------------------------------
2004-11-18 webertj 2004-11-18 imports (new syntax for theory headers)
2004-11-18 berghofe 2004-11-18 Tuned.
2004-11-17 kleing 2004-11-17 replace strangely encode space characters by  
2004-11-17 kleing 2004-11-17 replaced strangely encoded space characters by  
2004-11-17 webertj 2004-11-17 removed explicit mentioning of zChaffs version number
2004-11-17 webertj 2004-11-17 minor changes (comments/code refactoring)
2004-11-17 kleing 2004-11-17 removed Exercises document (available on separate web site now)
2004-11-17 kleing 2004-11-17 removed exercised document
2004-11-16 aspinall 2004-11-16 Markup obtain as introducing a nested goal.
2004-11-15 paulson 2004-11-15 removed a "clone" (duplicate code)
2004-11-15 webertj 2004-11-15 minor rewording
2004-11-15 aspinall 2004-11-15 Add <undoitem> for theory-state undos.
2004-11-15 paulson 2004-11-15 Renamed some variables to eliminate conflicts with constants. Introduced some abbreviations (following TPTP axiom sets) to reduce the amount of repetition. Uncommented some examples, which increases the runtime somewhat.
2004-11-14 webertj 2004-11-14 *** empty log message ***
2004-11-14 webertj 2004-11-14 DOCTYPE declaration added
2004-11-13 webertj 2004-11-13 Exercises added
2004-11-13 nipkow 2004-11-13 More lemmas
2004-11-12 webertj 2004-11-12 minor code refactoring
2004-11-12 paulson 2004-11-12 improved "subscribe" link
2004-11-12 webertj 2004-11-12 added DOCTYPE and Content-Type declarations to make this a valid HTML file
2004-11-12 webertj 2004-11-12 isatool usedir -f
2004-11-11 paulson 2004-11-11 updated subscription wording and link
2004-11-11 paulson 2004-11-11 increased tracing and search bounds
2004-11-08 paulson 2004-11-08 tidied comments
2004-11-05 schirmer 2004-11-05 * extended interface of record_split_simp_tac and record_split_simproc * improved record_type_abbr_tr'
2004-11-02 chaieb 2004-11-02 user-interface impoved
2004-10-29 paulson 2004-10-29 fixed some awkward problems with nat/int simprocs
2004-10-29 paulson 2004-10-29 fixed reference to renamed theorem
2004-10-28 webertj 2004-10-28 isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
2004-10-28 aspinall 2004-10-28 Make <undostep> call undos_proof to display resulting proofstate.
2004-10-28 chaieb 2004-10-28 efficienty improvement Heuristic is now the same as for the proof-generating alg.
2004-10-27 aspinall 2004-10-27 Revert change to pgml_sym
2004-10-27 berghofe 2004-10-27 Added type constraint to make SML/NJ happy.