| Tue, 02 Mar 2010 22:13:32 +0100 |
bulwahn |
adding HOL-Mutabelle to tests
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 17:45:10 +0100 |
krauss |
removed obsolete helper theory
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:34:40 +0100 |
haftmann |
renamed theory Rational to Rat
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 17:55:00 +0100 |
hoelzl |
merged
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 17:33:03 +0100 |
hoelzl |
Moved old Integration to examples.
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 14:11:32 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 10:11:31 +0100 |
haftmann |
dropped session W0; c.f. MiniML in AFP
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 08:04:07 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 16:03:44 +0100 |
haftmann |
added missing separator
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 15:53:18 +0100 |
haftmann |
distributed theory Algebras to theories Groups and Lattices
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 20:41:49 +0100 |
hoelzl |
Replaced Integration by Multivariate-Analysis/Real_Integration
|
file |
diff |
annotate
|
| Sat, 20 Feb 2010 23:23:04 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
file |
diff |
annotate
|
| Tue, 16 Feb 2010 15:25:36 +0100 |
boehmes |
added Cache_IO: cache for output of external tools,
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 19:37:34 +0100 |
wenzelm |
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 14:12:02 +0100 |
haftmann |
revert uninspired Structure_Syntax experiment
|
file |
diff |
annotate
|
| Tue, 09 Feb 2010 17:06:05 +0100 |
blanchet |
merged (manual for "nitpick_hol.ML" and "kodkod.ML")
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:27:21 +0100 |
blanchet |
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
|
file |
diff |
annotate
|
| Thu, 04 Feb 2010 16:03:15 +0100 |
blanchet |
split "nitpick_hol.ML" into two files to make it more manageable;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 21:26:52 +0100 |
wenzelm |
more precise dependencies;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:08:32 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:41 +0100 |
haftmann |
separate library theory for type classes combining lattices with various algebraic structures
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 10:36:02 +0100 |
haftmann |
separate theory for index structures
|
file |
diff |
annotate
|
| Tue, 02 Feb 2010 19:30:08 +0100 |
boehmes |
updated dependencies
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Mon, 25 Jan 2010 16:19:42 +0100 |
bulwahn |
adding Mutabelle to repository
|
file |
diff |
annotate
|
| Fri, 22 Jan 2010 15:26:29 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Wed, 20 Jan 2010 11:56:45 +0100 |
bulwahn |
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
|
file |
diff |
annotate
|
| Fri, 22 Jan 2010 13:38:29 +0100 |
haftmann |
more accurate dependencies
|
file |
diff |
annotate
|