equal
deleted
inserted
replaced
87 |
87 |
88 Presently, ISAC uses a slightly different representation for terms (which soon |
88 Presently, ISAC uses a slightly different representation for terms (which soon |
89 will disappear), which does not encode numerals as binary numbers: |
89 will disappear), which does not encode numerals as binary numbers: |
90 \<close> |
90 \<close> |
91 ML \<open> |
91 ML \<open> |
92 val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; |
92 val t = ParseC.parse_test (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; |
93 \<close> |
93 \<close> |
94 text \<open>From the above we see: the internal representation of a term contains |
94 text \<open>From the above we see: the internal representation of a term contains |
95 all the knowledge it is built from, see |
95 all the knowledge it is built from, see |
96 http://isabelle.in.tum.de/dist/library/HOL/Groups.html for the definitions |
96 http://isabelle.in.tum.de/dist/library/HOL/Groups.html for the definitions |
97 \begin{itemize} |
97 \begin{itemize} |
113 Without these theories Isabelle cannot do any thing, it even does not understand '+' or '*'. |
113 Without these theories Isabelle cannot do any thing, it even does not understand '+' or '*'. |
114 For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is |
114 For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is |
115 defined ('=' etc), but not yet '+' and '*', so you get 'NONE': |
115 defined ('=' etc), but not yet '+' and '*', so you get 'NONE': |
116 \<close> |
116 \<close> |
117 ML \<open> |
117 ML \<open> |
118 val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; |
118 val t = ParseC.parse_test (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; |
119 \<close> |
119 \<close> |
120 text \<open>ISAC uses comparatively few definitions and theorems from Isabelle, see |
120 text \<open>ISAC uses comparatively few definitions and theorems from Isabelle, see |
121 \begin{itemize} |
121 \begin{itemize} |
122 \item http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html |
122 \item http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html |
123 \end{itemize} |
123 \end{itemize} |