equal
deleted
inserted
replaced
78 inspection. Thus ISAC provides additional features, as we see below. First |
78 inspection. Thus ISAC provides additional features, as we see below. First |
79 let us store the term in a variable 't': |
79 let us store the term in a variable 't': |
80 \<close> |
80 \<close> |
81 ML \<open> |
81 ML \<open> |
82 val t = @{term "a + b * 9"}; |
82 val t = @{term "a + b * 9"}; |
83 TermC.atomwy t; |
83 TermC.atom_write_detail @{context} t; |
84 \<close> |
84 \<close> |
85 text \<open>Please, observe that in this case (whenever 'writeln' is involved, even |
85 text \<open>Please, observe that in this case (whenever 'writeln' is involved, even |
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 |