equal
deleted
inserted
replaced
108 id_apply[THEN eq_reflection] |
108 id_apply[THEN eq_reflection] |
109 id_def[THEN eq_reflection, symmetric] |
109 id_def[THEN eq_reflection, symmetric] |
110 id_o[THEN eq_reflection] |
110 id_o[THEN eq_reflection] |
111 o_id[THEN eq_reflection] |
111 o_id[THEN eq_reflection] |
112 |
112 |
|
113 |
|
114 (* The translation functions for the lifting process. *) |
|
115 use "quotient_term.ML" |
|
116 |
|
117 |
113 (* Definition of the quotient types *) |
118 (* Definition of the quotient types *) |
114 use "quotient_typ.ML" |
119 use "quotient_typ.ML" |
115 |
120 |
116 |
121 |
117 (* Definitions for quotient constants *) |
122 (* Definitions for quotient constants *) |
118 use "quotient_def.ML" |
123 use "quotient_def.ML" |
119 |
|
120 |
|
121 (* The translation functions for the lifting process. *) |
|
122 use "quotient_term.ML" |
|
123 |
|
124 |
124 |
125 (* Tactics for proving the lifted theorems *) |
125 (* Tactics for proving the lifted theorems *) |
126 |
126 |
127 lemma eq_imp_rel: |
127 lemma eq_imp_rel: |
128 "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
128 "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |