equal
deleted
inserted
replaced
142 ML {* |
142 ML {* |
143 fun lift_thm_my_int lthy t = |
143 fun lift_thm_my_int lthy t = |
144 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t |
144 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t |
145 *} |
145 *} |
146 |
146 |
147 lemma plus_sym_pre: |
|
148 shows "intrel (my_plus a b) (my_plus b a)" |
|
149 apply (cases a) |
|
150 apply (cases b) |
|
151 apply (simp) |
|
152 done |
|
153 |
|
154 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} |
147 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} |
155 |
148 |
156 lemma plus_assoc_pre: |
149 lemma plus_assoc_pre: |
157 shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))" |
150 shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))" |
158 apply (cases i) |
151 apply (cases i) |