equal
deleted
inserted
replaced
151 "Abs \<equiv> ABS_my_int" |
151 "Abs \<equiv> ABS_my_int" |
152 abbreviation |
152 abbreviation |
153 "Rep \<equiv> REP_my_int" |
153 "Rep \<equiv> REP_my_int" |
154 abbreviation |
154 abbreviation |
155 "Resp \<equiv> Respects" |
155 "Resp \<equiv> Respects" |
|
156 |
|
157 thm apply_rsp rep_abs_rsp lambda_prs |
|
158 ML {* map (Pattern.pattern o bare_concl o prop_of) @{thms apply_rsp rep_abs_rsp lambda_prs} *} |
156 |
159 |
157 |
160 |
158 lemma "PLUS a b = PLUS a b" |
161 lemma "PLUS a b = PLUS a b" |
159 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
162 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
160 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
163 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |