16 "----------- fun result, fun creates_assms ---------------------------------------------------"; |
16 "----------- fun result, fun creates_assms ---------------------------------------------------"; |
17 "----------- fun result, fun creates_assms ---------------------------------------------------"; |
17 "----------- fun result, fun creates_assms ---------------------------------------------------"; |
18 val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2}); |
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)) |
19 val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list)) |
20 ; |
20 ; |
21 Rewrite': ThyC.id * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T; |
21 Rewrite': ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T; |
22 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res) |
22 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res) |
23 ; |
23 ; |
24 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED"; |
24 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED"; |
25 if (Tactic.creates_assms tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED"; |
25 if (Tactic.creates_assms tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED"; |