History log of /seL4-l4v-master/isabelle/src/ZF/Induct/Primrec.thy
Revision Date Author Comments
# a4bab154 04-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# 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;


# 42fa88e3 09-Oct-2014 wenzelm <none@none>

proper @{cite} with bibtex entry (unchecked comment);


# fff34851 07-Oct-2014 wenzelm <none@none>

more antiquotations;


# 4a9ed335 07-Oct-2014 wenzelm <none@none>

more bibtex entries;
more antiquotations;


# 458a4961 13-Mar-2010 wenzelm <none@none>

removed old CVS Ids;
tuned headers;


# 04640bf0 11-Feb-2008 wenzelm <none@none>

removed unnecessary theory qualifiers;


# 4754b723 11-Feb-2008 krauss <none@none>

Made theory names in ZF disjoint from HOL theory names to allow loading both developments
in a single session (but not merge them).


# e7a16ceb 07-Oct-2007 wenzelm <none@none>

modernized specifications;
removed legacy ML bindings;


# 3daff02d 07-Oct-2007 wenzelm <none@none>

replaced some 'translations' by 'abbreviation';


# 7517dca8 11-Sep-2006 wenzelm <none@none>

induct method: renamed 'fixing' to 'arbitrary';


# e1c7ecf1 17-May-2006 wenzelm <none@none>

renamed CONST to CONSTANT;


# 8922a0f2 15-Dec-2005 wenzelm <none@none>

improved proofs;


# a7060872 17-Jun-2005 haftmann <none@none>

migrated theory headers to new format


# 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.


# 6ab7a33a 29-Dec-2001 wenzelm <none@none>

tuned document sources;


# a17994c0 20-Dec-2001 paulson <none@none>

converted some ZF/Induct examples to Isar


# d9ede52b 06-Nov-2001 paulson <none@none>

reorganization of the ZF examples