equal
deleted
inserted
replaced
124 subsection \<open>Prepare Expression\label{prep-expr}\<close> |
124 subsection \<open>Prepare Expression\label{prep-expr}\<close> |
125 text\<open>\noindent We try two different notations and check which of them |
125 text\<open>\noindent We try two different notations and check which of them |
126 Isabelle can handle best.\<close> |
126 Isabelle can handle best.\<close> |
127 ML \<open> |
127 ML \<open> |
128 val ctxt = Proof_Context.init_global @{theory}; |
128 val ctxt = Proof_Context.init_global @{theory}; |
129 val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt; |
129 (*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*) |
130 |
130 |
131 val SOME fun1 = |
131 val SOME fun1 = |
132 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1; |
132 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1; |
133 val SOME fun1' = |
133 val SOME fun1' = |
134 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1'; |
134 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1'; |