equal
deleted
inserted
replaced
86 invisibly) the output of 'atomwy t' is placed on top of the 'Output' window. |
86 invisibly) the output of 'atomwy t' is placed on top of the 'Output' window. |
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>val SOME t = TermC.parse @{theory "Isac_Knowledge"} "a + b * 3"; |
91 ML \<open> |
92 TermC.atomwy (Thm.term_of t); |
92 val t = TermC.parseNEW' (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} |
112 |
112 |
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>TermC.parse @{theory "HOL"} "a + b * 3"; |
117 ML \<open> |
|
118 val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; |
118 \<close> |
119 \<close> |
119 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 |
120 \begin{itemize} |
121 \begin{itemize} |
121 \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 |
122 \end{itemize} |
123 \end{itemize} |