| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
455aefc7 |
|
24-Jun-2018 |
wenzelm <none@none> |
simplified ZF theory names (in contrast to 6a0801279f4c): session-qualification already achieves disjointness;
--HG--
rename : src/ZF/Datatype_ZF.thy => src/ZF/Datatype.thy
rename : src/ZF/Inductive_ZF.thy => src/ZF/Inductive.thy
rename : src/ZF/Int_ZF.thy => src/ZF/Int.thy
rename : src/ZF/IntDiv_ZF.thy => src/ZF/IntDiv.thy
rename : src/ZF/List_ZF.thy => src/ZF/List.thy
rename : src/ZF/Nat_ZF.thy => src/ZF/Nat.thy
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
eea43a21 |
|
30-Dec-2015 |
wenzelm <none@none> |
clarified syntax;
|
| #
2531ee45 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
68f43bed |
|
23-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
| #
2257dcda |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
f902d62a |
|
06-Mar-2012 |
paulson <none@none> |
mathematical symbols instead of ASCII
|
| #
29168e90 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
ce5f42df |
|
29-Jul-2008 |
ballarin <none@none> |
Zorn's Lemma for partial orders.
|
| #
4754b723 |
|
11-Feb-2008 |
krauss <none@none> |
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
in a single session (but not merge them).
|
| #
e7a16ceb |
|
07-Oct-2007 |
wenzelm <none@none> |
modernized specifications;
removed legacy ML bindings;
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
04246c0e |
|
21-Apr-2004 |
wenzelm <none@none> |
constdefs: proper order;
|
| #
7654e199 |
|
27-Aug-2003 |
skalberg <none@none> |
Extended the notion of letter and digit, such that now one may use greek,
gothic, euler, or calligraphic letters as normal letters.
|
| #
6f50ca35 |
|
23-Jan-2003 |
paulson <none@none> |
tidying (by script)
|
| #
d2599419 |
|
03-Sep-2002 |
paulson <none@none> |
tidied
|
| #
d9f65115 |
|
14-Jul-2002 |
paulson <none@none> |
improved presentation markup
|
| #
7aca62df |
|
02-Jul-2002 |
paulson <none@none> |
Tidying and introduction of various new theorems
|
| #
7eb302a3 |
|
23-May-2002 |
paulson <none@none> |
new definition of "apply" and new simprule "beta_if"
|
| #
1f651d0f |
|
10-May-2002 |
paulson <none@none> |
converted the AC branch to Isar
|
| #
b5894316 |
|
28-Dec-1998 |
paulson <none@none> |
new inductive, datatype and primrec packages, etc.
|
| #
49ebaab4 |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs
|
| #
cc52541b |
|
09-Dec-1995 |
clasohm <none@none> |
removed quotes from consts and syntax sections
|
| #
da37c2f7 |
|
22-Jun-1995 |
clasohm <none@none> |
removed \...\ inside strings
|
| #
f9516776 |
|
19-Dec-1994 |
lcp <none@none> |
removed quotes around "Inductive"
|
| #
38ec27bf |
|
28-Nov-1994 |
lcp <none@none> |
replaced "rules" by "defs"
|
| #
37eef679 |
|
24-Aug-1994 |
lcp <none@none> |
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail
ZF/Makefile: now has Inductive.thy,.ML
ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils
|
| #
9df696ad |
|
11-Aug-1994 |
lcp <none@none> |
installation of new inductive/datatype sections
|
| #
199800bc |
|
26-Jul-1994 |
lcp <none@none> |
Axiom of choice, cardinality results, etc.
|