History log of /seL4-l4v-master/isabelle/src/ZF/Constructible/WFrec.thy
Revision Date Author Comments
# 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