src/HOL/IMP/Hoare.ML
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Fri, 17 Oct 1997 15:25:12 +0200 nipkow setloop split_tac -> addsplits
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Mon, 29 Sep 1997 12:13:43 +0200 paulson Step_tac -> Safe_tac
Wed, 23 Apr 1997 11:18:29 +0200 paulson Ran expandshort
Wed, 02 Apr 1997 11:30:48 +0200 paulson Replaced Best_tac by the one rule needed for the proof
Tue, 18 Mar 1997 18:02:19 +0100 nipkow Added wp_while.
Mon, 07 Oct 1996 10:26:00 +0200 paulson Ran expandshort
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Tue, 10 Sep 1996 20:10:29 +0200 nipkow Converted proofs to use default clasets.
Mon, 19 Aug 1996 11:17:20 +0200 paulson Tidied some proofs, maybe using less_SucE
Fri, 17 May 1996 12:24:47 +0200 nipkow Had to rename params because variable names in an induction rule changed.
Tue, 07 May 1996 18:19:13 +0200 paulson Updated for new form of induction rules
Sat, 27 Apr 1996 18:47:31 +0200 nipkow A completely new version of IMP.
Fri, 09 Feb 1996 13:41:59 +0100 nipkow Introduced qed_spec_mp.
Wed, 07 Feb 1996 12:22:32 +0100 nipkow Modified datatype com.
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Tue, 23 Jan 1996 10:59:35 +0100 nipkow Added a verified verification-condition generator.
Wed, 04 Oct 1995 13:12:14 +0100 clasohm added local simpsets
Tue, 09 May 1995 22:10:48 +0200 nipkow Moved induct2 from Hoare to Lfp.
Fri, 24 Mar 1995 12:30:35 +0100 clasohm changed syntax of tuples from <..., ...> to (..., ...)
Tue, 07 Mar 1995 15:00:34 +0100 nipkow *** empty log message ***
Tue, 07 Mar 1995 14:57:37 +0100 nipkow Hoare logic
less more (0) tip