| 2007-10-07 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| 2005-06-17 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| 2004-06-08 |
paulson |
Groups, Rings and supporting lemmas
|
file |
diff |
annotate
|
| 2003-08-27 |
skalberg |
Extended the notion of letter and digit, such that now one may use greek,
|
file |
diff |
annotate
|
| 2003-07-10 |
paulson |
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
|
file |
diff |
annotate
|
| 2003-06-30 |
paulson |
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
|
file |
diff |
annotate
|
| 2003-06-27 |
paulson |
Conversion of theory UNITY to Isar script
|
file |
diff |
annotate
|
| 2003-06-27 |
paulson |
Conversion of AllocBase to new-style
|
file |
diff |
annotate
|
| 2003-06-24 |
paulson |
Converting ZF/UNITY to Isar
|
file |
diff |
annotate
|
| 2003-05-27 |
paulson |
updating ZF-UNITY with Sidi's new material
|
file |
diff |
annotate
|
| 2003-04-23 |
paulson |
Got rid of the [iff], which was effectively inserting converseD
|
file |
diff |
annotate
|
| 2002-10-01 |
paulson |
Numerous cosmetic changes, prompted by the new simplifier
|
file |
diff |
annotate
|
| 2002-09-30 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| 2002-08-28 |
paulson |
various new lemmas for Constructible
|
file |
diff |
annotate
|
| 2002-07-14 |
paulson |
Removal of mono.thy
|
file |
diff |
annotate
|
| 2002-07-14 |
paulson |
improved presentation markup
|
file |
diff |
annotate
|
| 2002-06-29 |
paulson |
conversion of many files to Isar format
|
file |
diff |
annotate
|
| 2002-06-26 |
paulson |
new theorems
|
file |
diff |
annotate
|
| 2002-06-05 |
paulson |
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
|
file |
diff |
annotate
|
| 2002-05-24 |
paulson |
new quantifier lemmas
|
file |
diff |
annotate
|
| 2002-05-22 |
paulson |
more tidying
|
file |
diff |
annotate
|
| 2002-05-22 |
paulson |
tidying up
|
file |
diff |
annotate
|
| 2002-05-21 |
paulson |
conversion of OrdQuant.ML to Isar
|
file |
diff |
annotate
|
| 2002-05-21 |
paulson |
converted domrange to Isar and merged with equalities
|
file |
diff |
annotate
|
| 2002-05-20 |
paulson |
conversion of equalities and WF to Isar
|
file |
diff |
annotate
|
| 1997-01-03 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| 1994-08-15 |
lcp |
ZF/equalities/Sigma_cons: new
|
file |
diff |
annotate
|
| 1993-11-16 |
clasohm |
made pseudo theories for all ML files;
|
file |
diff |
annotate
|