| #
8ebe4ac4 |
|
18-Mar-2020 |
wenzelm <none@none> |
prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as proposed by Pedro Sánchez Terraf;
|
| #
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;
|
| #
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;
|
| #
2900a456 |
|
21-Jun-2007 |
wenzelm <none@none> |
tuned proofs -- avoid implicit prems;
|
| #
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
| #
ce4ef54e |
|
07-Nov-2006 |
wenzelm <none@none> |
tuned specifications;
|
| #
0c7ce443 |
|
20-Jun-2006 |
ballarin <none@none> |
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
23c64d47 |
|
06-Feb-2003 |
paulson <none@none> |
changed ** to ## to avoid conflict with new comment syntax
|
| #
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
|
| #
a511f8d9 |
|
18-Oct-2002 |
paulson <none@none> |
Tidying up. New primitives is_iterates and is_iterates_fm.
|
| #
02dd1b23 |
|
09-Oct-2002 |
paulson <none@none> |
Re-organization of Constructible theories
|
| #
78dc91f1 |
|
11-Sep-2002 |
paulson <none@none> |
Streamlined proofs of instances of Separation
|
| #
cfab4ca9 |
|
03-Sep-2002 |
paulson <none@none> |
deleted redundant material (quasiformula, ...) and rationalized
|
| #
8edc1796 |
|
27-Aug-2002 |
wenzelm <none@none> |
*** empty log message ***
|
| #
f625916c |
|
16-Aug-2002 |
paulson <none@none> |
Relativized right up to L satisfies V=L!
|
| #
a348dd1f |
|
15-Aug-2002 |
paulson <none@none> |
Tidying up
|
| #
78fd195f |
|
15-Aug-2002 |
paulson <none@none> |
Relativization and absoluteness for DPow!!
|
| #
5dc4a713 |
|
14-Aug-2002 |
paulson <none@none> |
Finished absoluteness of "satisfies"!!
|
| #
91850d5f |
|
13-Aug-2002 |
paulson <none@none> |
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
the new theory Internalize.thy
|
| #
6e930c1a |
|
13-Aug-2002 |
paulson <none@none> |
new file Constructible/Satisfies_absolute.thy
|