separate realpow constant, with additional cases not covered by Transcendental.powr;
1 (* Title: "ProgLang/calculate.sml"
2 Author: Walther Neuper 2021
3 (c) copyright due to lincense terms.
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
10 "-----------------------------------------------------------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "-----------------------------------------------------------------------------------------------";
14 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
15 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
16 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
18 fun test thy t = writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul thy t)));
20 test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;
21 test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;
22 test \<^theory> \<^term>\<open>10 * 20 :: real\<close>;
23 test \<^theory> \<^term>\<open>10 \<up> 20 :: real\<close>;
25 test \<^theory> \<^term>\<open>10 + 20 :: int\<close>;
26 test \<^theory> \<^term>\<open>10 - 20 :: int\<close>;
27 test \<^theory> \<^term>\<open>10 * 20 :: int\<close>;
29 test \<^theory> \<^term>\<open>10 + 20 :: nat\<close>;
30 test \<^theory> \<^term>\<open>10 - 20 :: nat\<close>;
31 test \<^theory> \<^term>\<open>10 * 20 :: nat\<close>;