equal
deleted
inserted
replaced
194 all_mem_range6 all_mem_range7 all_mem_range8 |
194 all_mem_range6 all_mem_range7 all_mem_range8 |
195 |
195 |
196 lemma pred_fun_True_id: "NO_MATCH id p \<Longrightarrow> pred_fun (\<lambda>x. True) p f = pred_fun (\<lambda>x. True) id (p \<circ> f)" |
196 lemma pred_fun_True_id: "NO_MATCH id p \<Longrightarrow> pred_fun (\<lambda>x. True) p f = pred_fun (\<lambda>x. True) id (p \<circ> f)" |
197 unfolding fun.pred_map unfolding comp_def id_def .. |
197 unfolding fun.pred_map unfolding comp_def id_def .. |
198 |
198 |
199 ML_file "Tools/BNF/bnf_lfp_util.ML" |
199 ML_file \<open>Tools/BNF/bnf_lfp_util.ML\<close> |
200 ML_file "Tools/BNF/bnf_lfp_tactics.ML" |
200 ML_file \<open>Tools/BNF/bnf_lfp_tactics.ML\<close> |
201 ML_file "Tools/BNF/bnf_lfp.ML" |
201 ML_file \<open>Tools/BNF/bnf_lfp.ML\<close> |
202 ML_file "Tools/BNF/bnf_lfp_compat.ML" |
202 ML_file \<open>Tools/BNF/bnf_lfp_compat.ML\<close> |
203 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" |
203 ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar_more.ML\<close> |
204 ML_file "Tools/BNF/bnf_lfp_size.ML" |
204 ML_file \<open>Tools/BNF/bnf_lfp_size.ML\<close> |
205 |
205 |
206 end |
206 end |