equal
deleted
inserted
replaced
34 abbreviation "Iface I == RefT (IfaceT I)" |
34 abbreviation "Iface I == RefT (IfaceT I)" |
35 abbreviation "Class C == RefT (ClassT C)" |
35 abbreviation "Class C == RefT (ClassT C)" |
36 abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) |
36 abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90) |
37 where "T.[] == RefT (ArrayT T)" |
37 where "T.[] == RefT (ArrayT T)" |
38 |
38 |
39 definition the_Class :: "ty \<Rightarrow> qtname" where |
39 definition |
40 "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **) |
40 the_Class :: "ty \<Rightarrow> qtname" |
|
41 where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **) |
41 |
42 |
42 lemma the_Class_eq [simp]: "the_Class (Class C)= C" |
43 lemma the_Class_eq [simp]: "the_Class (Class C)= C" |
43 by (auto simp add: the_Class_def) |
44 by (auto simp add: the_Class_def) |
44 |
45 |
45 end |
46 end |