equal
deleted
inserted
replaced
3 |
3 |
4 (* call_sim_tac invokes oracle "Sim" *) |
4 (* call_sim_tac invokes oracle "Sim" *) |
5 fun call_sim_tac thm_list i state = |
5 fun call_sim_tac thm_list i state = |
6 let val sign = #sign (rep_thm state); |
6 let val sign = #sign (rep_thm state); |
7 val (subgoal::_) = Library.drop(i-1,prems_of state); |
7 val (subgoal::_) = Library.drop(i-1,prems_of state); |
8 val OraAss = invoke_oracle MuIOAOracle.thy "Sim" (sign,SimOracleExn (subgoal,thm_list)); |
8 val OraAss = sim_oracle sign (subgoal,thm_list); |
9 in |
9 in |
10 (cut_facts_tac [OraAss] i) state |
10 (cut_facts_tac [OraAss] i) state |
11 end; |
11 end; |
12 |
12 |
13 (* is_sim_tac makes additionally to call_sim_tac some simplifications, |
13 (* is_sim_tac makes additionally to call_sim_tac some simplifications, |