equal
deleted
inserted
replaced
77 [(bCterm,Credex),(aCterm,aiCterm)] move_thm; |
77 [(bCterm,Credex),(aCterm,aiCterm)] move_thm; |
78 in |
78 in |
79 ((rtac inst_move_thm i) THEN (dtac eq_reflection i) |
79 ((rtac inst_move_thm i) THEN (dtac eq_reflection i) |
80 THEN (move_mus i)) state |
80 THEN (move_mus i)) state |
81 end |
81 end |
82 end; (* outer let *) |
82 end; |
83 end; (* local *) |
83 end; |
84 |
84 |
85 |
85 |
86 (* Type of call_mucke_tac has changed: an argument t of type thy was inserted (TH); *) |
|
87 (* Normally t can be user-instantiated by the value thy of the Isabelle context *) |
|
88 fun call_mucke_tac i state = |
86 fun call_mucke_tac i state = |
89 let val thy = Thm.theory_of_thm state; |
87 let val thy = Thm.theory_of_thm state; |
90 val (subgoal::_) = Library.drop(i-1,prems_of state); |
88 val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state)) |
91 val OraAss = mc_mucke_oracle thy subgoal; |
|
92 in |
89 in |
93 (cut_facts_tac [OraAss] i) state |
90 (cut_facts_tac [OraAss] i) state |
94 end; |
91 end; |
95 |
92 |
96 |
93 |