equal
deleted
inserted
replaced
166 |
166 |
167 thm i2.th_x thm i3.th_x |
167 thm i2.th_x thm i3.th_x |
168 |
168 |
169 ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *} |
169 ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *} |
170 |
170 |
171 lemma (in ID) th_y: "d == (a = b)" by fact |
171 lemma (in ID) th_y: "d == (a = b)" by (rule d_def) |
172 |
172 |
173 thm i2.th_y thm i3.th_y |
173 thm i2.th_y thm i3.th_y |
174 |
174 |
175 ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *} |
175 ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *} |
176 |
176 |