| 2015-12-30 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-07-23 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-03-23 |
wenzelm |
prefer local fixes;
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| 2012-03-06 |
paulson |
mathematical symbols instead of ASCII
|
file |
diff |
annotate
|
| 2011-11-20 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| 2009-10-17 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| 2008-07-29 |
ballarin |
Zorn's Lemma for partial orders.
|
file |
diff |
annotate
|
| 2008-02-11 |
krauss |
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
|
file |
diff |
annotate
|
| 2007-10-07 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| 2005-06-17 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| 2004-04-22 |
wenzelm |
constdefs: proper order;
|
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-01-23 |
paulson |
tidying (by script)
|
file |
diff |
annotate
|
| 2002-09-03 |
paulson |
tidied
|
file |
diff |
annotate
|
| 2002-07-14 |
paulson |
improved presentation markup
|
file |
diff |
annotate
|
| 2002-07-02 |
paulson |
Tidying and introduction of various new theorems
|
file |
diff |
annotate
|
| 2002-05-23 |
paulson |
new definition of "apply" and new simprule "beta_if"
|
file |
diff |
annotate
|
| 2002-05-10 |
paulson |
converted the AC branch to Isar
|
file |
diff |
annotate
|
| 1998-12-28 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
| 1996-02-06 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| 1995-12-09 |
clasohm |
removed quotes from consts and syntax sections
|
file |
diff |
annotate
|
| 1995-06-22 |
clasohm |
removed \...\ inside strings
|
file |
diff |
annotate
|
| 1994-12-19 |
lcp |
removed quotes around "Inductive"
|
file |
diff |
annotate
|
| 1994-11-28 |
lcp |
replaced "rules" by "defs"
|
file |
diff |
annotate
|
| 1994-08-25 |
lcp |
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
|
file |
diff |
annotate
|
| 1994-08-12 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
| 1994-07-26 |
lcp |
Axiom of choice, cardinality results, etc.
|
file |
diff |
annotate
|