equal
deleted
inserted
replaced
295 THEN' (rtac @{thm CollectI}) (* unfold comprehension *) |
295 THEN' (rtac @{thm CollectI}) (* unfold comprehension *) |
296 THEN' (fn i => REPEAT (rtac @{thm exI} i)) (* Turn existentials into schematic Vars *) |
296 THEN' (fn i => REPEAT (rtac @{thm exI} i)) (* Turn existentials into schematic Vars *) |
297 THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *) |
297 THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *) |
298 ORELSE' ((rtac @{thm conjI}) |
298 ORELSE' ((rtac @{thm conjI}) |
299 THEN' (rtac @{thm refl}) |
299 THEN' (rtac @{thm refl}) |
300 THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *) |
300 THEN' (blast_tac ctxt))) (* Solve rest of context... not very elegant *) |
301 ) i |
301 ) i |
302 in |
302 in |
303 ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)]) |
303 ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)]) |
304 THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st |
304 THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st |
305 end |
305 end |