| Mon, 29 Oct 2007 10:37:09 +0100 |
krauss |
fun/function: generate case names for induction rules
|
file |
diff |
annotate
|
| Fri, 14 Sep 2007 15:27:12 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 18:19:00 +0200 |
paulson |
new fun declaration
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 09:23:14 +0200 |
haftmann |
expanded fragile proof
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 05:18:39 +0200 |
huffman |
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 03:31:11 +0200 |
huffman |
removed constant int :: nat => int;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 11:06:04 +0200 |
chaieb |
tuned Proof
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Mon, 31 Jul 2006 21:06:40 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 11 Nov 2005 10:50:43 +0100 |
chaieb |
a proof step corrected due to the changement in the presburger method.
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Fri, 25 Mar 2005 16:20:57 +0100 |
paulson |
tidied up
|
file |
diff |
annotate
|
| Fri, 14 Jan 2005 12:00:27 +0100 |
nipkow |
made diff_less a simp rule
|
file |
diff |
annotate
|
| Thu, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
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
|
| Mon, 15 Oct 2001 20:42:06 +0200 |
wenzelm |
setsum syntax;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
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
|
| Tue, 07 Aug 2001 16:36:52 +0200 |
paulson |
Tweaks for 1 -> 1'
|
file |
diff |
annotate
|
| Mon, 25 Jun 2001 15:35:59 +0200 |
paulson |
Simprocs for type "nat" no longer introduce numerals unless they are already
|
file |
diff |
annotate
|
| Sun, 04 Feb 2001 19:31:13 +0100 |
wenzelm |
HOL-NumberTheory: converted to new-style format and proper document setup;
|
file |
diff |
annotate
|
| Tue, 03 Oct 2000 22:37:16 +0200 |
wenzelm |
tuned deps;
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 18:46:45 +0200 |
paulson |
moved Primes, Fib, Factorization from HOL/ex
|
file |
diff |
annotate
|