| Thu, 31 May 2001 16:50:13 +0200 |
oheimb |
added Least_Suc2
|
file |
diff |
annotate
|
| Thu, 15 Feb 2001 16:01:07 +0100 |
oheimb |
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
|
file |
diff |
annotate
|
| Wed, 10 Jan 2001 11:14:30 +0100 |
paulson |
generalizing the LEAST theorems from "nat" to linear
|
file |
diff |
annotate
|
| Wed, 20 Dec 2000 12:14:26 +0100 |
paulson |
tidying, removing obsolete lemmas about 0=... and 1=...
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 11:02:55 +0100 |
paulson |
renamed less_eq_Suc_add to less_imp_Suc_add
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:18:14 +0100 |
wenzelm |
nat_distrib;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2000 12:24:12 +0200 |
paulson |
got rid of a swap
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 12:39:57 +0200 |
paulson |
renamed (most of...) the select rules
|
file |
diff |
annotate
|
| Wed, 06 Sep 2000 08:04:41 +0200 |
nipkow |
less_induct -> nat_less_induct
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 12:02:01 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| 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
|
| Wed, 21 Aug 1996 11:00:04 +0200 |
paulson |
Added le_eq_less_Suc; fixed some comments;
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:49:31 +0200 |
paulson |
Now less_zeroE is a Safe Elim rule
|
file |
diff |
annotate
|
| Tue, 25 Jun 1996 13:11:29 +0200 |
berghofe |
Changed argument order of nat_rec.
|
file |
diff |
annotate
|
| Fri, 21 Jun 1996 13:51:09 +0200 |
berghofe |
Replaced occurrence of fast_tac by Fast_tac .
|
file |
diff |
annotate
|
| Thu, 20 Jun 1996 10:26:13 +0200 |
paulson |
Corrected comment
|
file |
diff |
annotate
|
| Mon, 03 Jun 1996 17:10:56 +0200 |
berghofe |
best_tac, deepen_tac and safe_tac now also use default claset.
|
file |
diff |
annotate
|
| Fri, 31 May 1996 19:34:40 +0200 |
oheimb |
renamed le_0 to le_0_eq, to avoid confusion with le0,
|
file |
diff |
annotate
|
| Thu, 23 May 1996 14:37:06 +0200 |
berghofe |
Replaced fast_tac by Fast_tac (which uses default claset)
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 17:34:05 +0200 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 16:58:21 +0200 |
oheimb |
repaired critical proofs depending on the order inside non-confluent SimpSets,
|
file |
diff |
annotate
|
| Wed, 17 Apr 1996 17:59:58 +0200 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 27 Mar 1996 18:45:17 +0100 |
paulson |
Library changes for mutilated checkerboard
|
file |
diff |
annotate
|
| Wed, 06 Mar 1996 12:52:11 +0100 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Mon, 04 Mar 1996 14:37:33 +0100 |
nipkow |
Added a constant UNIV == {x.True}
|
file |
diff |
annotate
|
| Fri, 09 Feb 1996 13:41:18 +0100 |
nipkow |
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:27:16 +0100 |
clasohm |
expanded tabs; renamed subtype to typedef;
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Sun, 12 Nov 1995 16:29:12 +0100 |
nipkow |
added new arithmetic lemmas and the functions take and drop.
|
file |
diff |
annotate
|
| Wed, 25 Oct 1995 09:48:29 +0100 |
nipkow |
Added various thms and tactics.
|
file |
diff |
annotate
|