| Tue, 08 Aug 2000 14:15:24 +0200 |
oheimb |
moved Hoare_example to Examples; other minor improvements
|
file |
diff |
annotate
|
| Tue, 04 Jul 2000 10:54:46 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 16:23:34 +0100 |
wenzelm |
case_tac now subsumes both boolean and datatype cases;
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 12:51:10 +0100 |
nipkow |
exhaust_tac -> cases_tac
|
file |
diff |
annotate
|
| Mon, 13 Dec 1999 10:54:04 +0100 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Fri, 12 Nov 1999 17:45:36 +0100 |
nipkow |
Added the proof by Nielson & Nielson.
|
file |
diff |
annotate
|
| Tue, 19 Jan 1999 11:18:11 +0100 |
paulson |
removal of the (thm list) argument of mk_cases
|
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
|
| Thu, 02 Apr 1998 17:19:02 +0200 |
oheimb |
split_all_tac now fails if there is nothing to split
|
file |
diff |
annotate
|
| Mon, 16 Mar 1998 16:50:50 +0100 |
paulson |
inverse -> converse
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 15:51:24 +0100 |
oheimb |
changed wrapper mechanism of classical reasoner
|
file |
diff |
annotate
|
| Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
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
|
| Tue, 17 Jun 1997 09:01:56 +0200 |
nipkow |
converse -> ^-1
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:18:29 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 17:52:31 +0100 |
oheimb |
reflecting my recent changes of the simplifier and classical reasoner
|
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
|
| Fri, 23 Aug 1996 13:03:02 +0200 |
nipkow |
Generalized my_lemma1: (c3,s3) |--> cs3
|
file |
diff |
annotate
|
| Tue, 07 May 1996 18:19:13 +0200 |
paulson |
Updated for new form of induction rules
|
file |
diff |
annotate
|
| Tue, 30 Apr 1996 17:32:29 +0200 |
nipkow |
Added an equivalence proof which avoids the use of -n->
|
file |
diff |
annotate
|
| Mon, 29 Apr 1996 20:15:33 +0200 |
nipkow |
Streamlined syntax: -(n)-> is now -n->.
|
file |
diff |
annotate
|
| Mon, 29 Apr 1996 15:48:27 +0200 |
nipkow |
Natural and Transition semantics.
|
file |
diff |
annotate
|