equal
deleted
inserted
replaced
1 theory QuotMain |
1 theory QuotMain |
2 imports QuotScript Prove |
2 imports QuotScript Prove |
3 uses ("quotient_info.ML") |
3 uses ("quotient_info.ML") |
4 ("quotient.ML") |
4 ("quotient_typ.ML") |
5 ("quotient_def.ML") |
5 ("quotient_def.ML") |
6 begin |
6 begin |
7 |
7 |
8 locale QUOT_TYPE = |
8 locale QUOT_TYPE = |
9 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
9 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
100 |
100 |
101 (* fun_map is not here since equivp is not true *) |
101 (* fun_map is not here since equivp is not true *) |
102 lemmas [quot_equiv] = identity_equivp |
102 lemmas [quot_equiv] = identity_equivp |
103 |
103 |
104 (* definition of the quotient types *) |
104 (* definition of the quotient types *) |
105 (* FIXME: should be called quotient_typ.ML *) |
105 use "quotient_typ.ML" |
106 use "quotient.ML" |
|
107 |
106 |
108 (* lifting of constants *) |
107 (* lifting of constants *) |
109 use "quotient_def.ML" |
108 use "quotient_def.ML" |
110 |
109 |
111 section {* Simset setup *} |
110 section {* Simset setup *} |