changeset 58390 | b74d8470b98e |
parent 58377 | c6f93b8d2d8e |
child 58391 | fe0fc8aee49a |
--- a/src/HOL/Basic_BNF_Least_Fixpoints.thy Fri Sep 19 13:27:04 2014 +0200 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy Fri Sep 19 13:27:04 2014 +0200 @@ -55,11 +55,7 @@ ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" -thm sum.rec_o_map -thm sum.size_o_map - -thm prod.rec_o_map -thm prod.size_o_map +ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML" hide_const (open) xtor ctor_rec