equal
deleted
inserted
replaced
203 ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
203 ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
204 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |
204 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |
205 ML_file "Tools/BNF/bnf_fp_n2m.ML" |
205 ML_file "Tools/BNF/bnf_fp_n2m.ML" |
206 ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML" |
206 ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML" |
207 |
207 |
208 ML_file "Tools/Function/size.ML" |
208 ML_file "Tools/Function/old_size.ML" |
209 setup Size.setup |
209 setup Old_Size.setup |
210 |
210 |
211 lemma size_bool[code]: "size (b\<Colon>bool) = 0" |
211 lemma size_bool[code]: "size (b\<Colon>bool) = 0" |
212 by (cases b) auto |
212 by (cases b) auto |
213 |
213 |
214 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n" |
214 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n" |