equal
deleted
inserted
replaced
10 ("quotient_def.ML") |
10 ("quotient_def.ML") |
11 ("quotient_term.ML") |
11 ("quotient_term.ML") |
12 ("quotient_tacs.ML") |
12 ("quotient_tacs.ML") |
13 begin |
13 begin |
14 |
14 |
15 locale Quot_Type = |
15 locale quot_type = |
16 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
16 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
17 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
17 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
18 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
18 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
19 assumes equivp: "equivp R" |
19 assumes equivp: "equivp R" |
20 and rep_prop: "\<And>y. \<exists>x. Rep y = R x" |
20 and rep_prop: "\<And>y. \<exists>x. Rep y = R x" |