History log of /seL4-l4v-master/l4v/isabelle/src/ZF/Induct/Binary_Trees.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;


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


# 2257dcda 02-Nov-2014 wenzelm <none@none>

modernized header;


# 8eca016b 13-Mar-2012 wenzelm <none@none>

tuned proofs;


# 001933f8 06-Mar-2012 paulson <none@none>

mathematical symbols for Isabelle/ZF example theories


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

removed old CVS Ids;
tuned headers;


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

modernized specifications;
removed legacy ML bindings;


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

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


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

improved proofs;


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

migrated theory headers to new format


# b804333b 20-Aug-2003 paulson <none@none>

new example


# 72d9d416 14-Nov-2001 wenzelm <none@none>

converted datatype examples moved from ZF/ex to ZF/Induct;