changeset 781 | f3a24012e9d8 |
parent 774 | b4ffb8826105 |
child 789 | 8237786171f1 |
--- a/Quot/QuotMain.thy Wed Dec 23 13:23:33 2009 +0100 +++ b/Quot/QuotMain.thy Wed Dec 23 13:45:42 2009 +0100 @@ -11,7 +11,7 @@ ("quotient_tacs.ML") begin -locale QUOT_TYPE = +locale Quot_Type = fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"