| #
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;
|
| #
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
|
| #
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;
|
| #
906d4fba |
|
26-Jun-2013 |
wenzelm <none@none> |
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac;
adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);
|
| #
ed870e69 |
|
15-Mar-2012 |
paulson <none@none> |
replacing ":" by "\<in>"
|
| #
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;
|
| #
828cfd22 |
|
15-Apr-2007 |
wenzelm <none@none> |
read prop as prop, not term;
|
| #
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
|
| #
4c207d95 |
|
08-Nov-2002 |
paulson <none@none> |
Polishing.
lambda_abs2 doesn't need an instance of replacement
various renamings & restructurings
|
| #
8caf2b2e |
|
29-Oct-2002 |
paulson <none@none> |
simpler separation/replacement proofs
|
| #
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
|
| #
71bc9cb6 |
|
10-Sep-2002 |
paulson <none@none> |
tweaks
|
| #
fd79e6e3 |
|
28-Aug-2002 |
paulson <none@none> |
completion of the consistency proof for AC
|
| #
8edc1796 |
|
27-Aug-2002 |
wenzelm <none@none> |
*** empty log message ***
|
| #
6b1bf3f8 |
|
21-Aug-2002 |
paulson <none@none> |
tweaked
|
| #
f625916c |
|
16-Aug-2002 |
paulson <none@none> |
Relativized right up to L satisfies V=L!
|
| #
925020bb |
|
31-Jul-2002 |
paulson <none@none> |
tweaks involving Separation
|
| #
7eb5606b |
|
30-Jul-2002 |
paulson <none@none> |
better sats rules for higher-order operators
|
| #
b7e6f188 |
|
28-Jul-2002 |
wenzelm <none@none> |
eliminate open locales and special ML code;
|
| #
3d9269f7 |
|
25-Jul-2002 |
paulson <none@none> |
More lemmas, working towards relativization of "satisfies"
|
| #
ce6a4938 |
|
24-Jul-2002 |
paulson <none@none> |
tweaks, aiming towards relativization of "satisfies"
|
| #
2ab802ef |
|
19-Jul-2002 |
paulson <none@none> |
Absoluteness of the function "nth"
|
| #
b096696b |
|
16-Jul-2002 |
wenzelm <none@none> |
adapted locales;
|
| #
77f354bf |
|
16-Jul-2002 |
paulson <none@none> |
instantiation of locales M_trancl and M_wfrank;
proofs of list_replacement{1,2}
|
| #
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.
|
| #
531cb224 |
|
09-Jul-2002 |
paulson <none@none> |
More relativization, reflection and proofs of separation
|
| #
f2094181 |
|
09-Jul-2002 |
paulson <none@none> |
More Separation proofs
|
| #
ba04d21f |
|
08-Jul-2002 |
paulson <none@none> |
more and simpler 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
|
| #
3283c84d |
|
04-Jul-2002 |
paulson <none@none> |
Constructible: some separation axioms
|
| #
6f081c47 |
|
04-Jul-2002 |
paulson <none@none> |
separation of M_axioms into M_triv_axioms and M_axioms
|
| #
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
|