| Sun, 23 Mar 2003 11:57:07 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 21 Mar 2003 18:15:56 +0100 |
paulson |
quadratic reciprocity files
|
file |
diff |
annotate
|
| Tue, 18 Mar 2003 18:07:06 +0100 |
paulson |
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
|
file |
diff |
annotate
|
| Tue, 11 Mar 2003 15:19:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 10 Mar 2003 16:21:06 +0100 |
paulson |
New theory ProgressSets. Definition of closure sets
|
file |
diff |
annotate
|
| Thu, 06 Mar 2003 15:08:38 +0100 |
paulson |
new UNITY examples theory
|
file |
diff |
annotate
|
| Tue, 18 Feb 2003 15:09:14 +0100 |
paulson |
new theory Transformers: Meier-Sanders non-interference theory
|
file |
diff |
annotate
|
| Fri, 31 Jan 2003 20:12:44 +0100 |
paulson |
conversion to new-style theories and tidying
|
file |
diff |
annotate
|
| Thu, 30 Jan 2003 18:08:09 +0100 |
paulson |
conversion of UNITY theories to new-style
|
file |
diff |
annotate
|
| Thu, 30 Jan 2003 10:35:56 +0100 |
paulson |
converting more UNITY theories to new-style
|
file |
diff |
annotate
|
| Wed, 29 Jan 2003 16:34:51 +0100 |
paulson |
converted more UNITY theories to new-style
|
file |
diff |
annotate
|
| Wed, 29 Jan 2003 11:02:08 +0100 |
paulson |
converting UNITY to new-style theories
|
file |
diff |
annotate
|
| Mon, 27 Jan 2003 10:39:31 +0100 |
kleing |
fixed missing UNITY files
|
file |
diff |
annotate
|
| Fri, 24 Jan 2003 14:06:49 +0100 |
paulson |
Partial conversion of UNITY to Isar new-style theories
|
file |
diff |
annotate
|
| Wed, 08 Jan 2003 13:49:52 +0100 |
nipkow |
New files in Hoare/
|
file |
diff |
annotate
|
| Wed, 11 Dec 2002 10:12:48 +0100 |
ballarin |
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
|
file |
diff |
annotate
|
| Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
file |
diff |
annotate
|
| Wed, 13 Nov 2002 15:26:19 +0100 |
berghofe |
Added inductive_realizer.
|
file |
diff |
annotate
|
| Sat, 09 Nov 2002 00:12:25 +0100 |
kleing |
Hoare.ML -> hoare.ML
|
file |
diff |
annotate
|
| Wed, 06 Nov 2002 14:02:18 +0100 |
nipkow |
Hoare.ML -> hoare.ML
|
file |
diff |
annotate
|
| Tue, 05 Nov 2002 15:59:17 +0100 |
kleing |
two new Bali files
|
file |
diff |
annotate
|
| Mon, 28 Oct 2002 14:29:51 +0100 |
nipkow |
conversion ML -> thy
|
file |
diff |
annotate
|
| Wed, 23 Oct 2002 16:09:02 +0200 |
streckem |
Added compiler
|
file |
diff |
annotate
|
| Fri, 27 Sep 2002 10:33:47 +0200 |
paulson |
New theory GroupTheory/Module.thy of modules
|
file |
diff |
annotate
|
| Thu, 26 Sep 2002 15:21:38 +0200 |
paulson |
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
|
file |
diff |
annotate
|
| Thu, 26 Sep 2002 10:51:29 +0200 |
paulson |
Converted Fun to Isar style.
|
file |
diff |
annotate
|
| Wed, 25 Sep 2002 07:57:36 +0200 |
nipkow |
Int.thy -> int.thy
|
file |
diff |
annotate
|
| Sat, 31 Aug 2002 14:03:49 +0200 |
paulson |
converted Hyperreal/Zorn to Isar format and moved to Library
|
file |
diff |
annotate
|
| Fri, 23 Aug 2002 07:41:05 +0200 |
nipkow |
Added div+mod cancelling simproc
|
file |
diff |
annotate
|
| Wed, 21 Aug 2002 15:53:30 +0200 |
paulson |
Frederic Blanqui's new "guard" examples
|
file |
diff |
annotate
|