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 wneuper <Walther.Neuper@jku.at>
Thu, 04 Aug 2022 12:48:37 +0200
changeset 60509 2e0b7ca391dc
parent 59937 c3f3123e8fbc
child 60574 3860f08122d8
permissions -rw-r--r--
polish naming in Rewrite_Order 
     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': 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)

    23 ;

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