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