equal
deleted
inserted
replaced
197 by (auto simp: base.cong_def step.equivp_gen_cong) |
197 by (auto simp: base.cong_def step.equivp_gen_cong) |
198 qed |
198 qed |
199 |
199 |
200 end |
200 end |
201 |
201 |
|
202 named_theorems friend_of_corec_simps |
|
203 |
202 ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML" |
204 ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML" |
203 ML_file "../Tools/BNF/bnf_gfp_grec.ML" |
205 ML_file "../Tools/BNF/bnf_gfp_grec.ML" |
204 ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML" |
206 ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML" |
205 ML_file "../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML" |
207 ML_file "../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML" |
206 ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML" |
208 ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML" |