Quot/QuotMain.thy
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)"