| Thu, 12 Oct 2000 13:01:19 +0200 |
nipkow |
induct -> lfp_induct
|
file |
diff |
annotate
|
| Wed, 11 Oct 2000 09:09:06 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 04 Jul 2000 10:54:46 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| Mon, 21 Sep 1998 12:01:14 +0200 |
oheimb |
simplified proof
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 16:15:37 +0200 |
oheimb |
streamlined proofs with new hoare_conseq1, hoare_conseq2
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:48:13 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Fri, 31 Jul 1998 10:48:42 +0200 |
paulson |
Removal of obsolete "open" commands from heads of .ML files
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Fri, 03 Jul 1998 10:36:47 +0200 |
nipkow |
Removed leading !! in goals.
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Wed, 06 May 1998 11:46:00 +0200 |
nipkow |
Changed [/] to [:=] and removed actual definition.
|
file |
diff |
annotate
|
| Sat, 07 Mar 1998 16:29:29 +0100 |
nipkow |
Removed `addsplits [expand_if]'
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 10:55:27 +0100 |
paulson |
Got rid of some slow deepen_tac calls
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 13:23:46 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 15:25:12 +0200 |
nipkow |
setloop split_tac -> addsplits
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 12:13:43 +0200 |
paulson |
Step_tac -> Safe_tac
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:18:29 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 11:30:48 +0200 |
paulson |
Replaced Best_tac by the one rule needed for the proof
|
file |
diff |
annotate
|
| Tue, 18 Mar 1997 18:02:19 +0100 |
nipkow |
Added wp_while.
|
file |
diff |
annotate
|
| Mon, 07 Oct 1996 10:26:00 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Tue, 10 Sep 1996 20:10:29 +0200 |
nipkow |
Converted proofs to use default clasets.
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:17:20 +0200 |
paulson |
Tidied some proofs, maybe using less_SucE
|
file |
diff |
annotate
|
| Fri, 17 May 1996 12:24:47 +0200 |
nipkow |
Had to rename params because variable names in an induction rule changed.
|
file |
diff |
annotate
|
| Tue, 07 May 1996 18:19:13 +0200 |
paulson |
Updated for new form of induction rules
|
file |
diff |
annotate
|
| Sat, 27 Apr 1996 18:47:31 +0200 |
nipkow |
A completely new version of IMP.
|
file |
diff |
annotate
|
| Fri, 09 Feb 1996 13:41:59 +0100 |
nipkow |
Introduced qed_spec_mp.
|
file |
diff |
annotate
|
| Wed, 07 Feb 1996 12:22:32 +0100 |
nipkow |
Modified datatype com.
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Tue, 23 Jan 1996 10:59:35 +0100 |
nipkow |
Added a verified verification-condition generator.
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:12:14 +0100 |
clasohm |
added local simpsets
|
file |
diff |
annotate
|
| Tue, 09 May 1995 22:10:48 +0200 |
nipkow |
Moved induct2 from Hoare to Lfp.
|
file |
diff |
annotate
|
| Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
| Tue, 07 Mar 1995 15:00:34 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 07 Mar 1995 14:57:37 +0100 |
nipkow |
Hoare logic
|
file |
diff |
annotate
|