| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Tue, 23 May 2000 18:28:11 +0200 |
paulson |
added type constraint ::nat because 0 is now overloaded
|
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
|
| Fri, 18 Feb 2000 20:24:56 +0100 |
oheimb |
added Suc_le_D
|
file |
diff |
annotate
|
| Mon, 10 Jan 2000 16:06:43 +0100 |
nipkow |
Forgot to "call" MicroJava in makefile.
|
file |
diff |
annotate
|
| Tue, 27 Jul 1999 17:19:31 +0200 |
paulson |
expandshort and tidying
|
file |
diff |
annotate
|
| Wed, 21 Jul 1999 15:23:18 +0200 |
paulson |
removed 2 qed_goals
|
file |
diff |
annotate
|
| Thu, 10 Jun 1999 10:34:55 +0200 |
paulson |
new lemma less_Suc_eq_0_disj
|
file |
diff |
annotate
|
| Thu, 15 Apr 1999 18:10:37 +0200 |
nipkow |
Added new thms.
|
file |
diff |
annotate
|
| Wed, 03 Mar 1999 11:15:18 +0100 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 12:16:34 +0100 |
nipkow |
Refined arithmetic.
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 08:41:28 +0100 |
nipkow |
Simplified arithmetic.
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 17:00:30 +0100 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
| Wed, 14 Oct 1998 11:50:48 +0200 |
nipkow |
Nat: added zero_neq_conv
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 18:14:26 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:34:59 +0200 |
berghofe |
Declaration of type 'nat' as a datatype (this allows usage of
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Sat, 07 Mar 1998 16:29:29 +0100 |
nipkow |
Removed `addsplits [expand_if]'
|
file |
diff |
annotate
|
| Wed, 23 Apr 1997 11:18:29 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Wed, 12 Feb 1997 18:53:59 +0100 |
nipkow |
New class "order" and accompanying changes.
|
file |
diff |
annotate
|
| Wed, 18 Dec 1996 15:10:33 +0100 |
oheimb |
added nat_induct2
|
file |
diff |
annotate
|
| Thu, 28 Nov 1996 12:09:33 +0100 |
nipkow |
Missing case in instantiation of Transitivity prover (negate(None)=None)
|
file |
diff |
annotate
|
| Thu, 07 Nov 1996 10:11:06 +0100 |
paulson |
Adding lessI to default claset
|
file |
diff |
annotate
|
| Mon, 21 Oct 1996 09:50:50 +0200 |
nipkow |
Added trans_tac (see Provers/nat_transitive.ML)
|
file |
diff |
annotate
|
| Wed, 16 Oct 1996 10:37:17 +0200 |
nipkow |
Defined pred using nat_case rather than nat_rec.
|
file |
diff |
annotate
|
| Thu, 10 Oct 1996 10:45:20 +0200 |
paulson |
Removed Fast_tac made redundant by addition of de Morgan laws
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Mon, 23 Sep 1996 18:12:45 +0200 |
paulson |
Addition of le_refl to default simpset/claset
|
file |
diff |
annotate
|
| Thu, 12 Sep 1996 10:40:05 +0200 |
paulson |
Tidied many proofs, using AddIffs to let equivalences take
|
file |
diff |
annotate
|