walther@60317: (* Title:  "ProgLang/calculate.sml"
walther@60317:    Author: Walther Neuper 2021
walther@60317:    (c) copyright due to lincense terms.
walther@60317: *)
walther@60317: 
walther@60317: "-----------------------------------------------------------------------------------------------";
walther@60317: "table of contents -----------------------------------------------------------------------------";
walther@60317: "-----------------------------------------------------------------------------------------------";
walther@60317: "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
walther@60317: "-----------------------------------------------------------------------------------------------";
walther@60317: "-----------------------------------------------------------------------------------------------";
walther@60317: "-----------------------------------------------------------------------------------------------";
walther@60317: 
walther@60317: "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
walther@60317: "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
walther@60317: "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
walther@60317: 
Walther@60509: fun test thy t = 
Walther@60509:   writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul @{context} t)));
walther@60317: 
walther@60401: test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;
walther@60401: test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;
walther@60401: test \<^theory> \<^term>\<open>10 * 20 :: real\<close>;
wenzelm@60405: test \<^theory> \<^term>\<open>10 \<up> 20 :: real\<close>;
walther@60401: 
walther@60401: test \<^theory> \<^term>\<open>10 + 20 :: int\<close>;
walther@60401: test \<^theory> \<^term>\<open>10 - 20 :: int\<close>;
walther@60401: test \<^theory> \<^term>\<open>10 * 20 :: int\<close>;
walther@60401: 
walther@60401: test \<^theory> \<^term>\<open>10 + 20 :: nat\<close>;
walther@60401: test \<^theory> \<^term>\<open>10 - 20 :: nat\<close>;
walther@60401: test \<^theory> \<^term>\<open>10 * 20 :: nat\<close>;