Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/MathEngBasic/tactic.sml
author Walther Neuper <walther.neuper@jku.at>
Sat, 30 Nov 2019 15:43:14 +0100
changeset 59728 f47a69ee4504
child 59850 f3cac3053e7b
permissions -rw-r--r--
lucin: prep. next_tactic_result, Accept_Tac2 takes ctxt in addition 
     1 (* Title:  "MathEngBasic/tactic.sml"

     2    Author: Walther Neuper

     3    (c) due to copyright terms

     4 *)

     5 

     6 "-----------------------------------------------------------------------------------------------";

     7 "table of contents -----------------------------------------------------------------------------";

     8 "-----------------------------------------------------------------------------------------------";

     9 "-----------------------------------------------------------------------------------------------";

    10 "----------- fun result, fun creates_assms ---------------------------------------------------";

    11 "-----------------------------------------------------------------------------------------------";

    12 "-----------------------------------------------------------------------------------------------";

    13 "-----------------------------------------------------------------------------------------------";

    14 

    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))

    20 ;

    21 Rewrite': theory' * rew_ord' * rls * bool * thm'' * term * result -> T;

    22 val tac = Rewrite' ("Diff", "dummy_ord", e_rls, true, thm'', f, res)

    23 ;

    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";
wneuper/isa