| Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
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
|
| 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
|
| Mon, 07 Dec 2009 14:54:01 +0100 |
haftmann |
merged Crude_Executable_Set into Executable_Set
|
file |
diff |
annotate
|
| Wed, 02 Dec 2009 17:53:34 +0100 |
haftmann |
added Crude_Executable_Set.thy
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 20:38:57 +0100 |
bulwahn |
added a tabled implementation of the reflexive transitive closure
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 13:59:49 +0100 |
haftmann |
moved Commutative_Ring into session Decision_Procs
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 11:19:24 +0100 |
haftmann |
re-moved theory Fin_Fun to AFP
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 09:03:57 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 13:23:18 +0200 |
himmelma |
distinguished session for multivariate analysis
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 17:12:36 +0200 |
haftmann |
turned off old quickcheck
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|