1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml	Sat Nov 30 15:43:14 2019 +0100
     1.3 @@ -0,0 +1,25 @@
     1.4 +(* Title:  "MathEngBasic/tactic.sml"
     1.5 +   Author: Walther Neuper
     1.6 +   (c) due to copyright terms
     1.7 +*)
     1.8 +
     1.9 +"-----------------------------------------------------------------------------------------------";
    1.10 +"table of contents -----------------------------------------------------------------------------";
    1.11 +"-----------------------------------------------------------------------------------------------";
    1.12 +"-----------------------------------------------------------------------------------------------";
    1.13 +"----------- fun result, fun creates_assms ---------------------------------------------------";
    1.14 +"-----------------------------------------------------------------------------------------------";
    1.15 +"-----------------------------------------------------------------------------------------------";
    1.16 +"-----------------------------------------------------------------------------------------------";
    1.17 +
    1.18 +"----------- fun result, fun creates_assms ---------------------------------------------------";
    1.19 +"----------- fun result, fun creates_assms ---------------------------------------------------";
    1.20 +"----------- fun result, fun creates_assms ---------------------------------------------------";
    1.21 +val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
    1.22 +val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
    1.23 +;
    1.24 +Rewrite': theory' * rew_ord' * rls * bool * thm'' * term * result -> T;
    1.25 +val tac = Rewrite' ("Diff", "dummy_ord", e_rls, true, thm'', f, res)
    1.26 +;
    1.27 +if (Tactic.result tac |> term2str) = "a / b" then () else error "creates_assms CHANGED";
    1.28 +if (Tactic.creates_assms tac |> terms2str) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";