| #
74c9a8d5 |
|
09-Apr-2017 |
wenzelm <none@none> |
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
--HG--
rename : src/ZF/Main_ZF.thy => src/ZF/ZF.thy
rename : src/ZF/Main_ZFC.thy => src/ZF/ZFC.thy
rename : src/ZF/ZF.thy => src/ZF/ZF_Base.thy
|
| #
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
db3d92c6 |
|
18-Feb-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids;
tuned headers;
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
6c6c8702 |
|
25-Dec-2001 |
paulson <none@none> |
conversion to Isar
|
| #
6e08acad |
|
31-May-2001 |
paulson <none@none> |
examples files start from Main instead of various ZF theories
|
| #
09045852 |
|
21-May-2001 |
paulson <none@none> |
X-symbols for ZF
|
| #
f9168499 |
|
13-Jan-1999 |
paulson <none@none> |
datatype package improvements
|
| #
8110d42e |
|
02-Apr-1997 |
paulson <none@none> |
Datatype declarations now require theory Datatype--NOT in quotes
|
| #
49ebaab4 |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs
|
| #
cc52541b |
|
09-Dec-1995 |
clasohm <none@none> |
removed quotes from consts and syntax sections
|
| #
54af57ee |
|
07-Mar-1995 |
lcp <none@none> |
Got rid of exvarU and constU by
including ExVar and Const in various datatype universes.
|
| #
8df51977 |
|
27-Feb-1995 |
lcp <none@none> |
New example by Jacob Frost, tidied by lcp
|