2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2002-05-07 wenzelm 2002-05-07 clarified eq_thm; added eq_thm_prop;
2002-05-06 nipkow 2002-05-06 Added insert_disjoint and disjoint_insert [simp], and simplified proofs
2002-05-04 berghofe 2002-05-04 Added skeletons to speed up rewriting on proof terms.
2002-04-30 kleing 2002-04-30 tuned
2002-04-30 kleing 2002-04-30 physical location of isabelle repository is now sunbroy2
2002-04-29 prensani 2002-04-29 added abstract;corrected RG_Basic Hoare rule.
2002-04-29 nipkow 2002-04-29 Better compiler proof
2002-04-29 nipkow 2002-04-29 Had to update proof for some strange reason
2002-04-29 nipkow 2002-04-29 added rev_take and rev_drop
2002-04-26 nipkow 2002-04-26 New machine architecture and other direction of compiler proof.
2002-04-25 nipkow 2002-04-25 added "m <= n ==> m-n = 0" [simp]
2002-04-19 berghofe 2002-04-19 code generator: wfrec combinator is now implemented by ML function wf_rec.
2002-04-19 berghofe 2002-04-19 Added example for code generation.
2002-04-19 berghofe 2002-04-19 wf is no longer implemented by true (due to change in definition of class_rec).
2002-04-19 berghofe 2002-04-19 Improved definition of class_rec: no longer mixes algorithm and termination check.
2002-04-19 berghofe 2002-04-19 Added proof of Newman's lemma.
2002-04-16 kleing 2002-04-16 new link to munich group
2002-04-16 kleing 2002-04-16 inserted tutorial
2002-04-16 nipkow 2002-04-16 *** empty log message ***
2002-04-15 paulson 2002-04-15 converted theory ex/Limit to Isar script, but it still needs work!
2002-04-15 paulson 2002-04-15 converted these theories to Isar format
2002-04-12 nipkow 2002-04-12 *** empty log message ***
2002-04-08 nipkow 2002-04-08 *** empty log message ***
2002-04-08 nipkow 2002-04-08 *** empty log message ***
2002-04-04 kleing 2002-04-04 tuned
2002-04-04 paulson 2002-04-04 conversion of Induct/{Slist,Sexp} to Isar scripts
2002-04-04 kleing 2002-04-04 flattened, uses locales
2002-04-04 kleing 2002-04-04 tuned
2002-04-03 oheimb 2002-04-03 bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
2002-04-02 paulson 2002-04-02 conversion of some HOL/Induct proof scripts to Isar
2002-04-02 nipkow 2002-04-02 Started to convert to locales
2002-03-28 berghofe 2002-03-28 mk_const_id now checks for clashes with reserved ML identifiers.
2002-03-27 kleing 2002-03-27 added lbv completeness
2002-03-27 kleing 2002-03-27 finished lbv completeness
2002-03-26 kleing 2002-03-26 merge mono
2002-03-26 kleing 2002-03-26 lub property of ++_f
2002-03-26 kleing 2002-03-26 +_f is associative and commutative
2002-03-24 kleing 2002-03-24 tuned
2002-03-24 kleing 2002-03-24 cleanup + simpler monotonicity
2002-03-24 kleing 2002-03-24 more about match_exception_table
2002-03-21 kleing 2002-03-21 first steps in semilattices..
2002-03-21 kleing 2002-03-21 new_Addr defined in terms of J/State.new_Addr (for compiler)
2002-03-20 kleing 2002-03-20 small refactoring for lbv with semilattices
2002-03-18 paulson 2002-03-18 Fewer premises for restrict_image
2002-03-14 paulson 2002-03-14 cambridge
2002-03-14 paulson 2002-03-14 removed ex/set.ML
2002-03-14 paulson 2002-03-14 converted theory "set" to Isar and added some SET-VAR examples
2002-03-14 kleing 2002-03-14 increased treshold for "this expression could be extremely ambigous" warning
2002-03-12 kleing 2002-03-12 workaround for "ins" bug in sml/nj + code generator
2002-03-12 nipkow 2002-03-12 *** empty log message ***
2002-03-11 wenzelm 2002-03-11 added Berhard Rumpe, Farhad Mehta;
2002-03-10 wenzelm 2002-03-10 tuned;
2002-03-09 kleing 2002-03-09 canonical start state
2002-03-09 kleing 2002-03-09 in wellformed programs, exceptions are classes
2002-03-08 wenzelm 2002-03-08 tuned;
2002-03-08 wenzelm 2002-03-08 tuned; Isabelle2002
2002-03-08 wenzelm 2002-03-08 tuned;
2002-03-08 wenzelm 2002-03-08 tuned;
2002-03-08 wenzelm 2002-03-08 removed Stanford mirror;