equal
deleted
inserted
replaced
9 begin |
9 begin |
10 |
10 |
11 datatype typerep = Typerep message_string "typerep list" |
11 datatype typerep = Typerep message_string "typerep list" |
12 |
12 |
13 class typerep = |
13 class typerep = |
14 fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep" |
14 fixes typerep :: "'a itself \<Rightarrow> typerep" |
15 begin |
15 begin |
16 |
16 |
17 definition typerep_of :: "'a \<Rightarrow> typerep" where |
17 definition typerep_of :: "'a \<Rightarrow> typerep" where |
18 [simp]: "typerep_of x = typerep TYPE('a)" |
18 [simp]: "typerep_of x = typerep TYPE('a)" |
19 |
19 |
77 |
77 |
78 end; |
78 end; |
79 *} |
79 *} |
80 |
80 |
81 setup {* |
81 setup {* |
82 Typerep.add_def @{type_name prop} |
82 Typerep.add_def @{type_name fun} |
83 #> Typerep.add_def @{type_name fun} |
|
84 #> Typerep.add_def @{type_name itself} |
83 #> Typerep.add_def @{type_name itself} |
85 #> Typerep.add_def @{type_name bool} |
84 #> Typerep.add_def @{type_name bool} |
86 #> TypedefPackage.interpretation Typerep.perhaps_add_def |
85 #> TypedefPackage.interpretation Typerep.perhaps_add_def |
87 *} |
86 *} |
88 |
87 |
90 "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2 |
89 "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2 |
91 \<and> list_all2 eq_class.eq tys1 tys2" |
90 \<and> list_all2 eq_class.eq tys1 tys2" |
92 by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric]) |
91 by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric]) |
93 |
92 |
94 code_type typerep |
93 code_type typerep |
95 (SML "Term.typ") |
94 (Eval "Term.typ") |
96 |
95 |
97 code_const Typerep |
96 code_const Typerep |
98 (SML "Term.Type/ (_, _)") |
97 (Eval "Term.Type/ (_, _)") |
99 |
98 |
100 code_reserved SML Term |
99 code_reserved Eval Term |
101 |
100 |
102 hide (open) const typerep Typerep |
101 hide (open) const typerep Typerep |
103 |
102 |
104 end |
103 end |