equal
deleted
inserted
replaced
125 |
125 |
126 subsection {*Prepare Expression\label{prep-expr}*} |
126 subsection {*Prepare Expression\label{prep-expr}*} |
127 text{*\noindent We try two different notations and check which of them |
127 text{*\noindent We try two different notations and check which of them |
128 Isabelle can handle best.*} |
128 Isabelle can handle best.*} |
129 ML {* |
129 ML {* |
130 val ctxt = ProofContext.init_global @{theory}; |
130 val ctxt = Proof_Context.init_global @{theory}; |
131 val ctxt = declare_constraints' [@{term "z::real"}] ctxt; |
131 val ctxt = declare_constraints' [@{term "z::real"}] ctxt; |
132 |
132 |
133 val SOME fun1 = |
133 val SOME fun1 = |
134 parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1; |
134 parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1; |
135 val SOME fun1' = |
135 val SOME fun1' = |
1612 \end{verbatim} |
1612 \end{verbatim} |
1613 The last but one line helps not to bother with ';'. |
1613 The last but one line helps not to bother with ';'. |
1614 \item Then we add line by line. Already the first line causes the error. |
1614 \item Then we add line by line. Already the first line causes the error. |
1615 So we investigate it by |
1615 So we investigate it by |
1616 \begin{verbatim} |
1616 \begin{verbatim} |
1617 val ctxt = ProofContext.init_global @{theory "Inverse_Z_Transform"} ; |
1617 val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ; |
1618 val SOME t = |
1618 val SOME t = |
1619 parseNEW ctxt "(num_orig::real) = |
1619 parseNEW ctxt "(num_orig::real) = |
1620 get_numerator(rhs f_f)"; |
1620 get_numerator(rhs f_f)"; |
1621 \end{verbatim} |
1621 \end{verbatim} |
1622 and see a type clash: \ttfamily rhs \normalfont from (1) requires type |
1622 and see a type clash: \ttfamily rhs \normalfont from (1) requires type |