equal
deleted
inserted
replaced
79 end); |
79 end); |
80 *} |
80 *} |
81 |
81 |
82 setup InductMethod.setup |
82 setup InductMethod.setup |
83 |
83 |
84 |
|
85 subsection {* Calculational rules *} |
|
86 |
|
87 lemma forw_subst: "a = b ==> P(b) ==> P(a)" |
|
88 by (rule ssubst) |
|
89 |
|
90 lemma back_subst: "P(a) ==> a = b ==> P(b)" |
|
91 by (rule subst) |
|
92 |
|
93 text {* |
|
94 Note that this list of rules is in reverse order of priorities. |
|
95 *} |
|
96 |
|
97 lemmas trans_rules [trans] = |
|
98 forw_subst |
|
99 back_subst |
|
100 rev_mp |
|
101 mp |
|
102 transitive |
|
103 trans |
|
104 |
|
105 lemmas [elim?] = sym |
|
106 |
|
107 end |
84 end |