equal
deleted
inserted
replaced
66 |
66 |
67 Isabelle does this differently by variables bound by a 'lambda' %, see |
67 Isabelle does this differently by variables bound by a 'lambda' %, see |
68 http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html |
68 http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html |
69 \<close> |
69 \<close> |
70 ML \<open> |
70 ML \<open> |
71 val t = @{term "%x. x^2 + x + y"}; TermC.atomwy t; UnparseC.term t; |
71 val t = @{term "%x. x^2 + x + y"}; |
|
72 TermC.atom_write_detail @{context} t; UnparseC.term_in_ctxt @{context} t; |
72 \<close> |
73 \<close> |
73 text \<open>Since this notation does not conform to present high-school matheatics |
74 text \<open>Since this notation does not conform to present high-school matheatics |
74 ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation |
75 ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation |
75 solving in ISAC. |
76 solving in ISAC. |
76 \<close> |
77 \<close> |