1 (* Title: "MathEngBasic/tactic.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "----------- fun result, fun creates_assms ---------------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "-----------------------------------------------------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
15 "----------- fun result, fun creates_assms ---------------------------------------------------";
16 "----------- fun result, fun creates_assms ---------------------------------------------------";
17 "----------- fun result, fun creates_assms ---------------------------------------------------";
18 val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
19 val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
21 Rewrite': theory' * Rule_Def.rew_ord' * rls * bool * thm'' * term * result -> T;
22 val tac = Rewrite' ("Diff", "dummy_ord", e_rls, true, thm'', f, res)
24 if (Tactic.result tac |> term2str) = "a / b" then () else error "creates_assms CHANGED";
25 if (Tactic.creates_assms tac |> terms2str) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";