src/HOL/BNF_Least_Fixpoint.thy
changeset 58182 82478e6c60cb
parent 58179 2de7b0313de3
child 58211 c1f3fa32d322
equal deleted inserted replaced
58181:6d527272f7b2 58182:82478e6c60cb
   186 ML_file "Tools/BNF/bnf_lfp.ML"
   186 ML_file "Tools/BNF/bnf_lfp.ML"
   187 ML_file "Tools/BNF/bnf_lfp_compat.ML"
   187 ML_file "Tools/BNF/bnf_lfp_compat.ML"
   188 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
   188 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
   189 ML_file "Tools/BNF/bnf_lfp_size.ML"
   189 ML_file "Tools/BNF/bnf_lfp_size.ML"
   190 ML_file "Tools/Function/old_size.ML"
   190 ML_file "Tools/Function/old_size.ML"
       
   191 ML_file "Tools/Old_Datatype/old_datatype_realizer.ML"
   191 
   192 
   192 lemma size_bool[code]: "size (b\<Colon>bool) = 0"
   193 lemma size_bool[code]: "size (b\<Colon>bool) = 0"
   193   by (cases b) auto
   194   by (cases b) auto
   194 
   195 
   195 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
   196 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"