2002-06-11 oheimb 2002-06-11 added the usual file headers
2002-06-11 kleing 2002-06-11 included strong soundness (sound + s0 <= phi!0)
2002-06-06 wenzelm 2002-06-06 updated;
2002-06-06 wenzelm 2002-06-06 examples;
2002-06-06 wenzelm 2002-06-06 updated;
2002-06-05 paulson 2002-06-05 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
2002-06-05 wenzelm 2002-06-05 initial setup;
2002-06-03 nipkow 2002-06-03 *** empty log message ***
2002-06-03 nipkow 2002-06-03 Added ex/MergeSort
2002-05-31 berghofe 2002-05-31 Added constants for Hyp, Oracle and MinProof.
2002-05-31 berghofe 2002-05-31 Changed interface of Pattern.rewrite_term.
2002-05-31 berghofe 2002-05-31 Changed interface of MetaSimplifier.rewrite_term.
2002-05-31 berghofe 2002-05-31 Changed interface of rewrite_term.
2002-05-31 berghofe 2002-05-31 Changes to rewrite_term: - now uses skeletons to speed up rewriting - added interface for rewriting procedures
2002-05-31 paulson 2002-05-31 conversion of Finite to Isar format
2002-05-31 paulson 2002-05-31 finished an incomplete proof
2002-05-31 paulson 2002-05-31 fixed a proof near the end
2002-05-31 nipkow 2002-05-31 *** empty log message ***
2002-05-31 nipkow 2002-05-31 *** empty log message ***
2002-05-31 nipkow 2002-05-31 Now arith can deal with div/mod arbitrary nat numerals.
2002-05-30 nipkow 2002-05-30 *** empty log message ***
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2002-05-30 nipkow 2002-05-30 Big update. Allows case splitting on ~= now (trying both < and >).
2002-05-28 paulson 2002-05-28 deleted some useless ML bindings
2002-05-28 paulson 2002-05-28 added <-> and ~
2002-05-28 paulson 2002-05-28 conversion of IntDiv.thy to Isar format
2002-05-28 berghofe 2002-05-28 Eps -> Hilbert_Choice.Eps
2002-05-27 nipkow 2002-05-27 *** empty log message ***
2002-05-24 paulson 2002-05-24 tidied; stronger lemmas about functions
2002-05-24 paulson 2002-05-24 strong lemmas about functions
2002-05-24 paulson 2002-05-24 new quantifier lemmas
2002-05-24 paulson 2002-05-24 converted Update to Isar
2002-05-24 paulson 2002-05-24 conversion of Perm to Isar. Strengthening of comp_fun_apply
2002-05-23 paulson 2002-05-23 new definition of "apply" and new simprule "beta_if"
2002-05-22 paulson 2002-05-22 more tidying
2002-05-22 paulson 2002-05-22 new version of nat_case, nat_case3
2002-05-22 paulson 2002-05-22 tidying up
2002-05-22 paulson 2002-05-22 conversion of Nat to Isar
2002-05-22 paulson 2002-05-22 tidied
2002-05-21 paulson 2002-05-21 conversion of OrdQuant.ML to Isar
2002-05-21 paulson 2002-05-21 converted domrange to Isar and merged with equalities
2002-05-20 paulson 2002-05-20 conversion of WF to Isar format
2002-05-20 paulson 2002-05-20 conversion of equalities to Isar
2002-05-20 paulson 2002-05-20 conversion of equalities and WF to Isar
2002-05-18 paulson 2002-05-18 converted Epsilon to Isar
2002-05-18 paulson 2002-05-18 converted Arith, Univ, func to Isar format!
2002-05-17 paulson 2002-05-17 New theorems from Constructible, and moving some Isar material from Main
2002-05-17 paulson 2002-05-17 unsymbolize
2002-05-17 paulson 2002-05-17 deleting the obsolete theorem lt_succ_iff
2002-05-17 nipkow 2002-05-17 Turned into Isar theories.
2002-05-17 nipkow 2002-05-17 *** empty log message ***
2002-05-17 nipkow 2002-05-17 allowed more general split rules to cope with div/mod 2
2002-05-17 nipkow 2002-05-17 Used to be Divides.ML
2002-05-16 paulson 2002-05-16 converting Ordinal.ML to Isar format
2002-05-15 nipkow 2002-05-15 Set up arith to deal with div 2 and mod 2.
2002-05-15 nipkow 2002-05-15 arith can now deal with div 2 and mod 2.
2002-05-15 nipkow 2002-05-15 Divides.ML -> Divides_lemmas.ML Converted Divides.thy to Isar.
2002-05-15 nipkow 2002-05-15 Removed superfluous thm
2002-05-15 paulson 2002-05-15 better error messages for datatypes not declared Const
2002-05-15 paulson 2002-05-15 better simplification of trivial existential equalities