equal
deleted
inserted
replaced
39 (Num 2 *** Var "x") +++ ((Num 2 *** Num 3) +++ Var "c"); |
39 (Num 2 *** Var "x") +++ ((Num 2 *** Num 3) +++ Var "c"); |
40 \<close> |
40 \<close> |
41 |
41 |
42 section \<open>Preview to Isabelle's terms\<close> |
42 section \<open>Preview to Isabelle's terms\<close> |
43 ML \<open> |
43 ML \<open> |
44 str2term; |
44 parse_test @{context}; |
45 str2term "234 * bbb + ccc"; |
45 parse_test @{context} "234 * bbb + ccc"; |
46 \<close> |
46 \<close> |
47 |
47 |
48 ML \<open> |
48 ML \<open> |
49 @{term "5"} |
49 @{term "5"} |
50 \<close> |
50 \<close> |