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/ProgLang/calculate.sml
author wneuper <Walther.Neuper@jku.at>
Mon, 01 Jan 2024 11:31:16 +0100
changeset 60789 8fa678b678e8
parent 60516 795d1352493a
permissions -rw-r--r--
Doc/Specify_Phase 4: start use antiquotations from isar-ref 
     1 (* Title:  "ProgLang/calculate.sml"

     2    Author: Walther Neuper 2021

     3    (c) copyright due to lincense terms.

     4 *)

     5 

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

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

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

     9 "----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";

    10 "-----------------------------------------------------------------------------------------------";

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

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

    13 

    14 "----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";

    15 "----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";

    16 "----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";

    17 

    18 fun test thy t = 

    19   writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, Calc_Binop.simplify @{context} t)));

    20 

    21 test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;

    22 test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;

    23 test \<^theory> \<^term>\<open>10 * 20 :: real\<close>;

    24 test \<^theory> \<^term>\<open>10 \<up> 20 :: real\<close>;

    25 

    26 test \<^theory> \<^term>\<open>10 + 20 :: int\<close>;

    27 test \<^theory> \<^term>\<open>10 - 20 :: int\<close>;

    28 test \<^theory> \<^term>\<open>10 * 20 :: int\<close>;

    29 

    30 test \<^theory> \<^term>\<open>10 + 20 :: nat\<close>;

    31 test \<^theory> \<^term>\<open>10 - 20 :: nat\<close>;

    32 test \<^theory> \<^term>\<open>10 * 20 :: nat\<close>;
wneuper/isa