equal
deleted
inserted
replaced
41 in |
41 in |
42 fold prepend_prem order all_tac |
42 fold prepend_prem order all_tac |
43 end |
43 end |
44 |
44 |
45 fun approximation_conv ctxt ct = |
45 fun approximation_conv ctxt ct = |
46 approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt)); |
46 approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct); |
47 |
47 |
48 fun approximate ctxt t = |
48 fun approximate ctxt t = |
49 approximation_oracle (Proof_Context.theory_of ctxt, t) |
49 approximation_oracle (Proof_Context.theory_of ctxt, t) |
50 |> Thm.prop_of |> Logic.dest_equals |> snd; |
50 |> Thm.prop_of |> Logic.dest_equals |> snd; |
51 |
51 |