equal
deleted
inserted
replaced
63 |
63 |
64 end |
64 end |
65 |
65 |
66 lemma sort_of_atom_name: |
66 lemma sort_of_atom_name: |
67 shows "sort_of (atom (a::name)) = Sort ''name'' []" |
67 shows "sort_of (atom (a::name)) = Sort ''name'' []" |
68 unfolding atom_name_def using Rep_name by simp |
68 by (simp add: atom_name_def Rep_name[simplified]) |
69 |
69 |
70 text {* Custom syntax for concrete atoms of type at *} |
70 text {* Custom syntax for concrete atoms of type at *} |
71 |
71 |
72 term "a:::name" |
72 term "a:::name" |
73 |
73 |
102 |
102 |
103 section {* Automatic instantiation of class @{text at}. *} |
103 section {* Automatic instantiation of class @{text at}. *} |
104 |
104 |
105 atom_decl name2 |
105 atom_decl name2 |
106 |
106 |
107 lemma sort_of_atom_name2: |
107 lemma |
108 "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []" |
108 "sort_of (atom (a::name2)) \<noteq> sort_of (atom (b::name))" |
109 unfolding atom_name2_def |
109 by (simp add: sort_of_atom_name) |
110 using Rep_name2 |
110 |
111 by simp |
|
112 |
111 |
113 text {* example swappings *} |
112 text {* example swappings *} |
114 lemma |
113 lemma |
115 fixes a b::"atom" |
114 fixes a b::"atom" |
116 assumes "sort_of a = sort_of b" |
115 assumes "sort_of a = sort_of b" |