| Wed, 06 Dec 2006 01:12:36 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 16:59:48 +0200 |
wenzelm |
axclass: name space prefix is now "c_class" instead of just "c";
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 15:06:20 +0200 |
paulson |
generlization of some "nat" theorems
|
file |
diff |
annotate
|
| Wed, 04 May 2005 08:36:10 +0200 |
nipkow |
Fixing a problem with lin.arith.
|
file |
diff |
annotate
|
| Wed, 15 Dec 2004 17:32:40 +0100 |
paulson |
removal of archaic Abs/Rep proofs
|
file |
diff |
annotate
|
| Mon, 29 Nov 2004 14:02:55 +0100 |
paulson |
converted to Isar script, simplifying some results
|
file |
diff |
annotate
|
| Sat, 27 Dec 2003 21:02:14 +0100 |
paulson |
re-organized numeric lemmas
|
file |
diff |
annotate
|
| Mon, 05 Aug 2002 14:27:55 +0200 |
berghofe |
Legacy ML bindings.
|
file |
diff |
annotate
|
| Wed, 31 Jul 2002 16:10:24 +0200 |
nipkow |
added mk_left_commute to HOL.thy and used it "everywhere"
|
file |
diff |
annotate
|
| Thu, 25 Apr 2002 17:36:29 +0200 |
nipkow |
added "m <= n ==> m-n = 0" [simp]
|
file |
diff |
annotate
|
| Tue, 26 Feb 2002 13:37:48 +0100 |
paulson |
Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
|
file |
diff |
annotate
|
| Mon, 25 Feb 2002 10:42:34 +0100 |
nipkow |
solved the problem that Larry's simproce cancle_numerals(?) returns
|
file |
diff |
annotate
|
| Thu, 13 Dec 2001 15:45:03 +0100 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| 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
|