equal
deleted
inserted
replaced
13 |
13 |
14 subsubsection {* Terms and class @{text term_of} *} |
14 subsubsection {* Terms and class @{text term_of} *} |
15 |
15 |
16 datatype "term" = dummy_term |
16 datatype "term" = dummy_term |
17 |
17 |
18 definition |
18 definition Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" where |
19 Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term" |
|
20 where |
|
21 "Const _ _ = dummy_term" |
19 "Const _ _ = dummy_term" |
22 |
20 |
23 definition |
21 definition App :: "term \<Rightarrow> term \<Rightarrow> term" where |
24 App :: "term \<Rightarrow> term \<Rightarrow> term" |
|
25 where |
|
26 "App _ _ = dummy_term" |
22 "App _ _ = dummy_term" |
27 |
23 |
28 code_datatype Const App |
24 code_datatype Const App |
29 |
25 |
30 class term_of = typerep + |
26 class term_of = typerep + |