equal
deleted
inserted
replaced
40 (* Isabelle goal to be proved), then transfer the reconstruction *) |
40 (* Isabelle goal to be proved), then transfer the reconstruction *) |
41 (* steps as a string to the input pipe of the main Isabelle process *) |
41 (* steps as a string to the input pipe of the main Isabelle process *) |
42 (**********************************************************************) |
42 (**********************************************************************) |
43 |
43 |
44 |
44 |
45 val atomize_tac = |
45 val atomize_tac = SUBGOAL |
46 SUBGOAL |
|
47 (fn (prop,_) => |
46 (fn (prop,_) => |
48 let val ts = Logic.strip_assums_hyp prop |
47 let val ts = Logic.strip_assums_hyp prop |
49 in EVERY1 |
48 in EVERY1 |
50 [METAHYPS |
49 [METAHYPS |
51 (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), |
50 (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), |