#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
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;
|
#
0551f7de |
|
01-Nov-2014 |
wenzelm <none@none> |
eliminated spurious semicolons;
|
#
f5cf0e45 |
|
06-Mar-2012 |
paulson <none@none> |
More mathematical symbols for ZF examples
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
#
ce4ef54e |
|
07-Nov-2006 |
wenzelm <none@none> |
tuned specifications;
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
a645e18a |
|
19-Nov-2002 |
paulson <none@none> |
stylistic tweaks
|
#
02dd1b23 |
|
09-Oct-2002 |
paulson <none@none> |
Re-organization of Constructible theories
|
#
32a75c4c |
|
01-Oct-2002 |
paulson <none@none> |
Numerous cosmetic changes, prompted by the new simplifier
|
#
57f1080b |
|
10-Sep-2002 |
paulson <none@none> |
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
|
#
5d3d4feb |
|
16-Aug-2002 |
paulson <none@none> |
Various tweaks of the presentation
|
#
f625916c |
|
16-Aug-2002 |
paulson <none@none> |
Relativized right up to L satisfies V=L!
|
#
b7e6f188 |
|
28-Jul-2002 |
wenzelm <none@none> |
eliminate open locales and special ML code;
|
#
b096696b |
|
16-Jul-2002 |
wenzelm <none@none> |
adapted locales;
|
#
2f5543d0 |
|
12-Jul-2002 |
paulson <none@none> |
towards relativization of "iterates" and "wfrec"
|
#
abeafcaa |
|
12-Jul-2002 |
paulson <none@none> |
new definitions of fun_apply and M_is_recfun
|
#
b1be672f |
|
11-Jul-2002 |
paulson <none@none> |
tidied
|
#
78e7d959 |
|
11-Jul-2002 |
paulson <none@none> |
Separation/Replacement up to M_wfrank!
|
#
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.
|
#
f2094181 |
|
09-Jul-2002 |
paulson <none@none> |
More Separation proofs
|
#
2f7f94f6 |
|
05-Jul-2002 |
paulson <none@none> |
more internalized formulas and separation proofs
|
#
9896925d |
|
04-Jul-2002 |
paulson <none@none> |
More use of relativized quantifiers
|
#
9afd489e |
|
04-Jul-2002 |
wenzelm <none@none> |
document setup;
|
#
056466d5 |
|
04-Jul-2002 |
paulson <none@none> |
tweaks
|
#
7aca62df |
|
02-Jul-2002 |
paulson <none@none> |
Tidying and introduction of various new theorems
|
#
53395f2a |
|
01-Jul-2002 |
paulson <none@none> |
more use of relativized quantifiers list_closed
|
#
9255eae1 |
|
28-Jun-2002 |
paulson <none@none> |
class quantifiers (some) absoluteness and closure for WFrec-defined functions
|
#
9988cebf |
|
26-Jun-2002 |
paulson <none@none> |
new treatment of wfrec, replacing wf[A](r) by wf(r)
|
#
24bfa3d1 |
|
26-Jun-2002 |
paulson <none@none> |
towards absoluteness of wfrec-defined functions
|
#
1d3f622d |
|
24-Jun-2002 |
paulson <none@none> |
development and tweaks
|
#
30f9b4f9 |
|
19-Jun-2002 |
paulson <none@none> |
new theory of inner models
|