equal
deleted
inserted
replaced
40 using not_fresh_nat_of [unfolded fresh_def] by auto |
40 using not_fresh_nat_of [unfolded fresh_def] by auto |
41 |
41 |
42 |
42 |
43 section {* Manual instantiation of class @{text at}. *} |
43 section {* Manual instantiation of class @{text at}. *} |
44 |
44 |
45 typedef (open) name = "{a. sort_of a = Sort ''name'' []}" |
45 typedef name = "{a. sort_of a = Sort ''name'' []}" |
46 by (rule exists_eq_simple_sort) |
46 by (rule exists_eq_simple_sort) |
47 |
47 |
48 instantiation name :: at |
48 instantiation name :: at |
49 begin |
49 begin |
50 |
50 |
141 apply(simp_all) |
141 apply(simp_all) |
142 done |
142 done |
143 |
143 |
144 declare sort_of_ty.simps [simp del] |
144 declare sort_of_ty.simps [simp del] |
145 |
145 |
146 typedef (open) var = "{a. sort_of a \<in> range sort_of_ty}" |
146 typedef var = "{a. sort_of a \<in> range sort_of_ty}" |
147 by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp) |
147 by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp) |
148 |
148 |
149 instantiation var :: at_base |
149 instantiation var :: at_base |
150 begin |
150 begin |
151 |
151 |