equal
deleted
inserted
replaced
111 unfolding sum_rel_def by simp+ |
111 unfolding sum_rel_def by simp+ |
112 |
112 |
113 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
113 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
114 by blast |
114 by blast |
115 |
115 |
|
116 lemma fun_rel_def_butlast: |
|
117 "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))" |
|
118 unfolding fun_rel_def .. |
|
119 |
116 ML_file "Tools/bnf_fp_util.ML" |
120 ML_file "Tools/bnf_fp_util.ML" |
117 ML_file "Tools/bnf_fp_def_sugar_tactics.ML" |
121 ML_file "Tools/bnf_fp_def_sugar_tactics.ML" |
118 ML_file "Tools/bnf_fp_def_sugar.ML" |
122 ML_file "Tools/bnf_fp_def_sugar.ML" |
119 |
123 |
120 end |
124 end |