| #
b0d86b76 |
|
04-Feb-2020 |
paulson <lp15@cam.ac.uk> |
Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf
|
| #
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;
|
| #
2257dcda |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
2400213a |
|
21-Mar-2012 |
paulson <none@none> |
refinements to constructibility
|
| #
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
|
| #
d75e992b |
|
15-Jan-2003 |
paulson <none@none> |
more new-style theories
|
| #
02dd1b23 |
|
09-Oct-2002 |
paulson <none@none> |
Re-organization of Constructible theories
|
| #
56765f7e |
|
04-Oct-2002 |
paulson <none@none> |
Various simplifications of the Constructible theories
|
| #
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.
|
| #
57f1080b |
|
10-Sep-2002 |
paulson <none@none> |
renamed M_triv_axioms to M_trivial and M_axioms to M_basic
|
| #
10b3b868 |
|
21-Aug-2002 |
paulson <none@none> |
tweaks
|
| #
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;
|
| #
abeafcaa |
|
12-Jul-2002 |
paulson <none@none> |
new definitions of fun_apply and M_is_recfun
|
| #
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.
|
| #
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
|
| #
3283c84d |
|
04-Jul-2002 |
paulson <none@none> |
Constructible: some separation axioms
|
| #
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
|
| #
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
|