equal
deleted
inserted
replaced
260 rewrite_goal_tac goal_ctxt [def] THEN' |
260 rewrite_goal_tac goal_ctxt [def] THEN' |
261 resolve_tac goal_ctxt [Drule.reflexive_thm])) |
261 resolve_tac goal_ctxt [Drule.reflexive_thm])) |
262 handle ERROR msg => cat_error msg "Failed to prove definitional specification"; |
262 handle ERROR msg => cat_error msg "Failed to prove definitional specification"; |
263 in |
263 in |
264 def_thm |
264 def_thm |
265 |> singleton (Variable.export def_ctxt def_ctxt0) |
265 |> singleton (Proof_Context.export def_ctxt def_ctxt0) |
266 |> Drule.zero_var_indexes |
266 |> Drule.zero_var_indexes |
267 end; |
267 end; |
268 in (((c, T), rhs), prove) end; |
268 in (((c, T), rhs), prove) end; |
269 |
269 |
270 end; |
270 end; |