equal
deleted
inserted
replaced
28 apply (intro Pure.equal_intr_rule) |
28 apply (intro Pure.equal_intr_rule) |
29 apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+ |
29 apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+ |
30 apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+ |
30 apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+ |
31 done |
31 done |
32 |
32 |
33 ML_file "cconv.ML" |
33 ML_file \<open>cconv.ML\<close> |
34 ML_file "rewrite.ML" |
34 ML_file \<open>rewrite.ML\<close> |
35 |
35 |
36 end |
36 end |