| Thu, 08 Dec 1994 12:50:38 +0100 | clasohm | replaced store_thm by bind_thm | file | diff | annotate |
| Wed, 07 Dec 1994 14:11:22 +0100 | nipkow | Removed a local lemma which is now part of HOL_ss. | file | diff | annotate |
| Mon, 21 Nov 1994 17:50:34 +0100 | clasohm | replaced 'val ... = result()' by 'qed "..."' | file | diff | annotate |
| Thu, 03 Nov 1994 11:36:54 +0100 | nipkow | Replaced fast_tac by simp_tac in a number of places. | file | diff | annotate |
| Wed, 07 Sep 1994 13:17:34 +0200 | lcp | HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster | file | diff | annotate |
| Tue, 06 Sep 1994 16:15:59 +0200 | nipkow | Converted rules to primrecs | file | diff | annotate |
| Wed, 31 Aug 1994 16:25:19 +0200 | nipkow | Renamed a few types and vars | file | diff | annotate |
| Wed, 31 Aug 1994 15:15:54 +0200 | nipkow | Equivalence of op. and den. sem. for simple while language. | file | diff | annotate |