keep obsolete interpretations in Main, to avoid merge trouble
authorblanchet
Fri Sep 19 13:27:04 2014 +0200 (2014-09-19)
changeset 58390b74d8470b98e
parent 58389 ee1f45ca0d73
child 58391 fe0fc8aee49a
keep obsolete interpretations in Main, to avoid merge trouble
src/HOL/Basic_BNF_Least_Fixpoints.thy
src/HOL/Code_Numeral.thy
src/HOL/Library/Old_Datatype.thy
     1.1 --- a/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Sep 19 13:27:04 2014 +0200
     1.2 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Fri Sep 19 13:27:04 2014 +0200
     1.3 @@ -55,11 +55,7 @@
     1.4  
     1.5  ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
     1.6  
     1.7 -thm sum.rec_o_map
     1.8 -thm sum.size_o_map
     1.9 -
    1.10 -thm prod.rec_o_map
    1.11 -thm prod.size_o_map
    1.12 +ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
    1.13  
    1.14  hide_const (open) xtor ctor_rec
    1.15  
     2.1 --- a/src/HOL/Code_Numeral.thy	Fri Sep 19 13:27:04 2014 +0200
     2.2 +++ b/src/HOL/Code_Numeral.thy	Fri Sep 19 13:27:04 2014 +0200
     2.3 @@ -809,15 +809,19 @@
     2.4    shows P
     2.5    using assms by transfer blast
     2.6  
     2.7 -instantiation natural :: size
     2.8 -begin
     2.9 +lemma [simp, code]: "size_natural = nat_of_natural"
    2.10 +proof (rule ext)
    2.11 +  fix n
    2.12 +  show "size_natural n = nat_of_natural n"
    2.13 +    by (induct n) simp_all
    2.14 +qed
    2.15  
    2.16 -definition size_natural :: "natural \<Rightarrow> nat" where
    2.17 -  [simp, code]: "size_natural = nat_of_natural"
    2.18 -
    2.19 -instance ..
    2.20 -
    2.21 -end
    2.22 +lemma [simp, code]: "size = nat_of_natural"
    2.23 +proof (rule ext)
    2.24 +  fix n
    2.25 +  show "size n = nat_of_natural n"
    2.26 +    by (induct n) simp_all
    2.27 +qed
    2.28  
    2.29  lemma natural_decr [termination_simp]:
    2.30    "n \<noteq> 0 \<Longrightarrow> nat_of_natural n - Nat.Suc 0 < nat_of_natural n"
     3.1 --- a/src/HOL/Library/Old_Datatype.thy	Fri Sep 19 13:27:04 2014 +0200
     3.2 +++ b/src/HOL/Library/Old_Datatype.thy	Fri Sep 19 13:27:04 2014 +0200
     3.3 @@ -10,7 +10,6 @@
     3.4  keywords "old_datatype" :: thy_decl
     3.5  begin
     3.6  
     3.7 -ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
     3.8  ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
     3.9  
    3.10