| Wed, 23 May 2007 02:50:19 +0200 |
huffman |
remove unused simproc definition
|
file |
diff |
annotate
|
| Wed, 23 May 2007 02:33:42 +0200 |
huffman |
remove redundant simproc; remove legacy ML bindings
|
file |
diff |
annotate
|
| Mon, 14 May 2007 18:48:24 +0200 |
huffman |
move lemmas to RealPow.thy; tuned proofs
|
file |
diff |
annotate
|
| Mon, 14 May 2007 09:33:18 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 13:15:12 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:13 +0200 |
wenzelm |
change_claset/simpset;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 17:16:52 +0200 |
wenzelm |
accomodate change of real_of_XXX;
|
file |
diff |
annotate
|
| Wed, 04 May 2005 10:42:43 +0200 |
nipkow |
fixed lin.arith
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:25:33 +0200 |
wenzelm |
reverted renaming of Some/None in comments and strings;
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Tue, 07 Sep 2004 13:41:30 +0200 |
nipkow |
fixed discrete field.
|
file |
diff |
annotate
|
| Mon, 06 Sep 2004 17:37:35 +0200 |
nipkow |
made mult_mono_thms generic.
|
file |
diff |
annotate
|
| Thu, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
file |
diff |
annotate
|
| Tue, 30 Mar 2004 11:25:14 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|