equal
deleted
inserted
replaced
11 |
11 |
12 subsection {* Term representation *} |
12 subsection {* Term representation *} |
13 |
13 |
14 subsubsection {* Terms and class @{text term_of} *} |
14 subsubsection {* Terms and class @{text term_of} *} |
15 |
15 |
16 datatype_new "term" = dummy_term |
16 datatype "term" = dummy_term |
17 |
17 |
18 definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where |
18 definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where |
19 "Const _ _ = dummy_term" |
19 "Const _ _ = dummy_term" |
20 |
20 |
21 definition App :: "term \<Rightarrow> term \<Rightarrow> term" where |
21 definition App :: "term \<Rightarrow> term \<Rightarrow> term" where |