equal
deleted
inserted
replaced
142 lift_thm lthy qty ty_name rsp_thms defs t |
142 lift_thm lthy qty ty_name rsp_thms defs t |
143 *} |
143 *} |
144 |
144 |
145 print_quotients |
145 print_quotients |
146 |
146 |
147 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} |
147 ML {* |
|
148 val test = lift_thm_my_int @{context} @{thm plus_sym_pre} |
|
149 *} |
|
150 |
|
151 ML {* my_lift (prop_of test) @{thm plus_sym_pre} @{context} *} |
|
152 |
|
153 ML {* |
|
154 ObjectLogic.atomize_term @{theory} (prop_of test) |
|
155 |> Syntax.string_of_term @{context} |
|
156 |> writeln |
|
157 *} |
148 |
158 |
149 lemma plus_assoc_pre: |
159 lemma plus_assoc_pre: |
150 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
160 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
151 apply (cases i) |
161 apply (cases i) |
152 apply (cases j) |
162 apply (cases j) |