IMP/Equiv.ML
Mon, 21 Nov 1994 17:50:34 +0100 clasohm replaced 'val ... = result()' by 'qed "..."'
Thu, 03 Nov 1994 11:36:54 +0100 nipkow Replaced fast_tac by simp_tac in a number of places.
Wed, 07 Sep 1994 13:17:34 +0200 lcp HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster
Tue, 06 Sep 1994 16:15:59 +0200 nipkow Converted rules to primrecs
Wed, 31 Aug 1994 16:25:19 +0200 nipkow Renamed a few types and vars
Wed, 31 Aug 1994 15:15:54 +0200 nipkow Equivalence of op. and den. sem. for simple while language.
less more (0) tip