src/HOL/IMP/Transition.ML
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-06-17 nipkow 1997-06-17 converse -> ^-1
1997-04-23 paulson 1997-04-23 Ran expandshort
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1996-10-07 paulson 1996-10-07 Ran expandshort
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-10 nipkow 1996-09-10 Converted proofs to use default clasets.
1996-08-23 nipkow 1996-08-23 Generalized my_lemma1: (c3,s3) |--> cs3
1996-05-07 paulson 1996-05-07 Updated for new form of induction rules
1996-04-30 nipkow 1996-04-30 Added an equivalence proof which avoids the use of -n-> (with help from Ranan Fraer)
1996-04-29 nipkow 1996-04-29 Streamlined syntax: -(n)-> is now -n->.
1996-04-29 nipkow 1996-04-29 Natural and Transition semantics.