src/HOL/IMP/Hoare.ML
Thu, 12 Oct 2000 13:01:19 +0200 nipkow induct -> lfp_induct
Wed, 11 Oct 2000 09:09:06 +0200 nipkow *** empty log message ***
Tue, 04 Jul 2000 10:54:46 +0200 oheimb disambiguated := ; added Examples (factorial)
Mon, 21 Sep 1998 12:01:14 +0200 oheimb simplified proof
Wed, 12 Aug 1998 16:15:37 +0200 oheimb streamlined proofs with new hoare_conseq1, hoare_conseq2
Thu, 06 Aug 1998 15:48:13 +0200 paulson even more tidying of Goal commands
Fri, 31 Jul 1998 10:48:42 +0200 paulson Removal of obsolete "open" commands from heads of .ML files
Fri, 24 Jul 1998 13:03:20 +0200 berghofe Adapted to new datatype package.
Fri, 03 Jul 1998 10:36:47 +0200 nipkow Removed leading !! in goals.
Mon, 22 Jun 1998 17:26:46 +0200 wenzelm isatool fixgoal;
Wed, 06 May 1998 11:46:00 +0200 nipkow Changed [/] to [:=] and removed actual definition.
Sat, 07 Mar 1998 16:29:29 +0100 nipkow Removed `addsplits [expand_if]'
Thu, 20 Nov 1997 10:55:27 +0100 paulson Got rid of some slow deepen_tac calls
Wed, 05 Nov 1997 13:23:46 +0100 paulson Ran expandshort, especially to introduce Safe_tac
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