| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
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
|
| #
eea43a21 |
|
30-Dec-2015 |
wenzelm <none@none> |
clarified syntax;
|
| #
2531ee45 |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
42e4d508 |
|
10-Oct-2015 |
wenzelm <none@none> |
tuned syntax -- more symbols;
|
| #
e52d778b |
|
23-Mar-2012 |
paulson <none@none> |
proof tidying
|
| #
001933f8 |
|
06-Mar-2012 |
paulson <none@none> |
mathematical symbols for Isabelle/ZF example theories
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
e92443e4 |
|
24-Jul-2008 |
haftmann <none@none> |
dropped locale (open)
|
| #
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
|
| #
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.
|
| #
4c5b9c69 |
|
23-Jul-2002 |
wenzelm <none@none> |
AC18: meta-level predicate via locale;
|
| #
afb97ade |
|
21-Jan-2002 |
paulson <none@none> |
lexical tidying
|
| #
f2952072 |
|
18-Jan-2002 |
paulson <none@none> |
tidied
|
| #
956fb34f |
|
16-Jan-2002 |
paulson <none@none> |
Isar version of AC
|
| #
1de2a707 |
|
18-Dec-2001 |
paulson <none@none> |
replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
by lesspoll_trans1, lesspoll_trans2
|
| #
17fc8a4f |
|
21-May-2001 |
paulson <none@none> |
X-symbols for set theory
|
| #
fdba0abf |
|
13-Jan-2000 |
paulson <none@none> |
a bit of tidying
|
| #
f3f91f1c |
|
03-Jan-1997 |
paulson <none@none> |
Implicit simpsets and clasets for FOL and ZF
|
| #
49ebaab4 |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs
|
| #
cc52541b |
|
09-Dec-1995 |
clasohm <none@none> |
removed quotes from consts and syntax sections
|
| #
e19c6bfd |
|
28-Jul-1995 |
lcp <none@none> |
Ran expandshort and changed spelling of Grabczewski
|
| #
da37c2f7 |
|
22-Jun-1995 |
clasohm <none@none> |
removed \...\ inside strings
|
| #
129a37a3 |
|
18-May-1995 |
lcp <none@none> |
Krzysztof Grabczewski's (nearly) complete AC proofs
|
| #
074767f5 |
|
25-Apr-1995 |
lcp <none@none> |
Simple updates for compatibility with KG
|
| #
bac78427 |
|
05-Apr-1995 |
lcp <none@none> |
Moved some local definitions to WO6_WO1.ML
|
| #
405a69f7 |
|
31-Mar-1995 |
lcp <none@none> |
New example of AC Equivalences by Krzysztof Grabczewski
|