History log of /seL4-l4v-master/isabelle/src/HOL/Tools/BNF/bnf_lfp_countable.ML
Revision Date Author Comments
# 14c7fb8f 09-Aug-2019 wenzelm <none@none>

formal position for PThm nodes;
# ed7a971e 05-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;
# a4bab154 04-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;
# 502ab55a 30-Dec-2016 blanchet <none@none>

more uniform errors in '(prim)(co)rec(ursive)' variants
# 659a2dbd 20-Dec-2016 blanchet <none@none>

generalized ML function (towards nonuniform datatypes)
# d945085c 12-Sep-2016 blanchet <none@none>

make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
# 9828cea0 21-Mar-2016 blanchet <none@none>

put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints

--HG--
rename : src/HOL/Library/bnf_axiomatization.ML => src/HOL/Tools/BNF/bnf_axiomatization.ML
rename : src/HOL/Library/bnf_lfp_countable.ML => src/HOL/Tools/BNF/bnf_lfp_countable.ML