equal
deleted
inserted
replaced
336 by simp |
336 by simp |
337 |
337 |
338 lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)" |
338 lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)" |
339 by auto |
339 by auto |
340 |
340 |
341 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
|
342 by blast |
|
343 |
|
344 ML_file "Tools/bnf_gfp_util.ML" |
341 ML_file "Tools/bnf_gfp_util.ML" |
345 ML_file "Tools/bnf_gfp_tactics.ML" |
342 ML_file "Tools/bnf_gfp_tactics.ML" |
346 ML_file "Tools/bnf_gfp.ML" |
343 ML_file "Tools/bnf_gfp.ML" |
347 |
344 |
348 end |
345 end |