Tue, 10 Jul 2007 17:30:49 +0200 |
haftmann |
clarified import
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 20:48:47 +0200 |
wenzelm |
moved Presburger setup back to Presburger.thy;
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 17:28:50 +0200 |
wenzelm |
renamed NatSimprocs.thy to Arith_Tools.thy;
|
file |
diff |
annotate
|
Sun, 06 May 2007 21:49:44 +0200 |
haftmann |
PreList imports RecDef
|
file |
diff |
annotate
|
Wed, 22 Nov 2006 10:20:17 +0100 |
haftmann |
does not import Hilber_Choice any longer
|
file |
diff |
annotate
|
Mon, 13 Nov 2006 15:43:07 +0100 |
haftmann |
PreList = Main - List
|
file |
diff |
annotate
|
Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 15:21:48 +0200 |
haftmann |
text cleanup
|
file |
diff |
annotate
|
Tue, 20 Sep 2005 14:03:37 +0200 |
wenzelm |
tuned theory dependencies;
|
file |
diff |
annotate
|
Tue, 09 Aug 2005 19:10:30 +0200 |
nipkow |
moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
|
file |
diff |
annotate
|
Fri, 08 Jul 2005 11:38:30 +0200 |
nipkow |
changed imports due to new GCD.thy
|
file |
diff |
annotate
|
Fri, 19 Nov 2004 14:00:31 +0100 |
chaieb |
Barith removed
|
file |
diff |
annotate
|
Wed, 06 Oct 2004 13:58:08 +0200 |
chaieb |
changed in order to insert Barith.thy
|
file |
diff |
annotate
|
Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
Fri, 16 Apr 2004 04:07:10 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
Thu, 24 Jul 2003 16:35:51 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
Tue, 25 Mar 2003 09:49:13 +0100 |
berghofe |
Added Presburger theory.
|
file |
diff |
annotate
|
Thu, 04 Jul 2002 16:48:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 21 Feb 2002 20:09:19 +0100 |
wenzelm |
removed theory Option;
|
file |
diff |
annotate
|
Tue, 05 Feb 2002 23:18:08 +0100 |
wenzelm |
moved SVC stuff to ex;
|
file |
diff |
annotate
|
Thu, 06 Dec 2001 00:39:40 +0100 |
wenzelm |
less_induct, wf_induct_rule;
|
file |
diff |
annotate
|
Wed, 28 Nov 2001 00:37:40 +0100 |
wenzelm |
tuned declarations;
|
file |
diff |
annotate
|
Fri, 02 Nov 2001 22:01:58 +0100 |
wenzelm |
theory Calculation move to Set;
|
file |
diff |
annotate
|
Sat, 27 Oct 2001 00:00:38 +0200 |
wenzelm |
moved product cases/induct to theory Datatype;
|
file |
diff |
annotate
|
Tue, 16 Oct 2001 17:51:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 15 Oct 2001 21:04:32 +0200 |
kleing |
canonical 'cases'/'induct' rules for n-tuples (n=3..7)
|
file |
diff |
annotate
|
Sat, 23 Dec 2000 22:50:39 +0100 |
wenzelm |
hide type node item;
|
file |
diff |
annotate
|
Fri, 15 Dec 2000 17:59:30 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
Thu, 14 Dec 2000 19:36:48 +0100 |
wenzelm |
added Summation;
|
file |
diff |
annotate
|
Fri, 24 Nov 2000 16:49:27 +0100 |
nipkow |
hide many names from Datatype_Universe.
|
file |
diff |
annotate
|
Wed, 18 Oct 2000 23:40:17 +0200 |
wenzelm |
tuned declarations;
|
file |
diff |
annotate
|
Thu, 12 Oct 2000 18:38:23 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Thu, 17 Aug 2000 10:33:37 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
Wed, 14 Jun 2000 17:59:53 +0200 |
wenzelm |
theorems [cases type: bool] = case_split;
|
file |
diff |
annotate
|
Fri, 12 May 2000 15:05:02 +0200 |
paulson |
NatSimprocs is now a theory, not a file
|
file |
diff |
annotate
|
Mon, 08 May 2000 20:59:30 +0200 |
wenzelm |
moved theory Sexp to Induct examples;
|
file |
diff |
annotate
|
Fri, 21 Apr 2000 11:28:18 +0200 |
paulson |
new file Integ/NatSimprocs.ML
|
file |
diff |
annotate
|
Fri, 24 Mar 2000 08:56:48 +0100 |
nipkow |
comments
|
file |
diff |
annotate
|
Thu, 16 Mar 2000 00:35:27 +0100 |
wenzelm |
added HOL/PreLIst.thy;
|
file |
diff |
annotate
|