| #
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
|
| #
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
|
| #
65e75de5 |
|
27-Jun-2003 |
paulson <none@none> |
Conversion of AllocBase to new-style
|
| #
b85a197d |
|
02-Jun-2003 |
paulson <none@none> |
Further tweaks of ZF/UNITY
|
| #
dd2a5068 |
|
27-May-2003 |
paulson <none@none> |
updating ZF-UNITY with Sidi's new material
|
| #
6f50ca35 |
|
23-Jan-2003 |
paulson <none@none> |
tidying (by script)
|
| #
32a75c4c |
|
01-Oct-2002 |
paulson <none@none> |
Numerous cosmetic changes, prompted by the new simplifier
|
| #
ceac7595 |
|
30-Sep-2002 |
berghofe <none@none> |
Adapted to new simplifier.
|
| #
647bcb01 |
|
27-Aug-2002 |
wenzelm <none@none> |
*** empty log message ***
|
| #
6f883b73 |
|
21-Aug-2002 |
paulson <none@none> |
new lemmas
|
| #
18a3b8c7 |
|
19-Jul-2002 |
paulson <none@none> |
A couple of new theorems for Constructible
|
| #
92ba76e1 |
|
18-Jul-2002 |
paulson <none@none> |
new theorems to support Constructible proofs
|
| #
d9f65115 |
|
14-Jul-2002 |
paulson <none@none> |
improved presentation markup
|
| #
78231b68 |
|
10-Jul-2002 |
paulson <none@none> |
Fixed quantified variable name preservation for ball and bex (bounded quants)
Requires tweaking of other scripts. Also routine tidying.
|
| #
c4673c54 |
|
09-Jul-2002 |
paulson <none@none> |
converted List to new-style
|
| #
d49e01e7 |
|
16-Jan-2002 |
paulson <none@none> |
new definitions from Sidi Ehmety
|
| #
0f036851 |
|
07-Aug-2000 |
paulson <none@none> |
instantiated Cancel_Numerals for "nat" in ZF
|
| #
ac826664 |
|
01-Aug-2000 |
paulson <none@none> |
natify, a coercion to reduce the number of type constraints in arithmetic
|
| #
0649249a |
|
07-Jan-1999 |
paulson <none@none> |
ZF: the natural numbers as a datatype
|
| #
b5894316 |
|
28-Dec-1998 |
paulson <none@none> |
new inductive, datatype and primrec packages, etc.
|
| #
daf66f30 |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed dots;
|
| #
d85df1e4 |
|
23-Jan-1997 |
wenzelm <none@none> |
turned some consts into syntax;
|
| #
1beac027 |
|
19-Aug-1996 |
paulson <none@none> |
Addition of function set_of_list
|
| #
ae702a91 |
|
17-Jun-1996 |
paulson <none@none> |
Converted to use constdefs instead of defs
|
| #
49ebaab4 |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs
|
| #
cc52541b |
|
09-Dec-1995 |
clasohm <none@none> |
removed quotes from consts and syntax sections
|
| #
87b873b9 |
|
19-Dec-1994 |
lcp <none@none> |
removed quotes around "Datatype",
and removed needless mention of [Q]Univ
|
| #
38ec27bf |
|
28-Nov-1994 |
lcp <none@none> |
replaced "rules" by "defs"
|
| #
8c53611e |
|
06-Sep-1994 |
lcp <none@none> |
removal of needless quotes
|
| #
9df696ad |
|
11-Aug-1994 |
lcp <none@none> |
installation of new inductive/datatype sections
|
| #
ba6b9f3c |
|
21-Jun-1994 |
lcp <none@none> |
Addition of cardinals and order types, various tidying
|
| #
5c777ea1 |
|
16-Nov-1993 |
clasohm <none@none> |
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
|