| Tue, 02 Sep 2008 22:37:20 +0200 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 12:01:59 +0200 |
haftmann |
added HOL/ex/Numeral.thy
|
file |
diff |
annotate
|
| Tue, 05 Aug 2008 14:40:48 +0200 |
krauss |
fix HOL/ex/LexOrds.thy; add to regression
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 19:03:33 +0200 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 16:16:10 +0200 |
ballarin |
New theory on divisibility;
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 14:07:23 +0200 |
haftmann |
corrected Pure dependency
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 15:26:23 +0200 |
haftmann |
(adjusted)
|
file |
diff |
annotate
|
| Wed, 16 Jul 2008 17:37:59 +0200 |
berghofe |
Added Standardization theory to nominal examples.
|
file |
diff |
annotate
|
| Fri, 04 Jul 2008 07:39:01 +0200 |
haftmann |
added marginal setup for code generation
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 19:50:19 +0200 |
wenzelm |
removed old Complex/ex/NSPrimes.thy;
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 19:17:29 +0200 |
wenzelm |
more precise dependencies for HOL-Word and HOL-NSA;
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 17:53:39 +0200 |
huffman |
add HOL-NSA
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 11:16:33 +0200 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 07:12:17 +0200 |
haftmann |
code antiquotation roaring ahead
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 21:20:18 +0200 |
wenzelm |
clean: HOL-Plain;
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 09:58:32 +0200 |
haftmann |
(removed Complex/ROOT.ML)
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 07:58:17 +0200 |
haftmann |
HOL += HOL-Complex
|
file |
diff |
annotate
|
| Mon, 30 Jun 2008 13:41:30 +0200 |
haftmann |
HOL-Complex with proof terms
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 15:51:38 +0200 |
wenzelm |
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 21:00:16 +0200 |
haftmann |
moved Float.thy to Library
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 11:51:47 +0200 |
wenzelm |
some reformatting;
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 10:03:45 +0200 |
urbanc |
added CK_Machine to the nominal section
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 19:15:20 +0200 |
wenzelm |
added HOL/Tools/induct_tacs.ML;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:06 +0200 |
haftmann |
major refactorings in code generator modules
|
file |
diff |
annotate
|
| Sun, 01 Jun 2008 17:39:21 +0200 |
urbanc |
new example
|
file |
diff |
annotate
|
| Tue, 13 May 2008 09:14:07 +0200 |
krauss |
fixed makefile
|
file |
diff |
annotate
|