# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261265213 -3600
# Node ID df053507edba2fcf88973371357cc096868253d3
# Parent  d0250d01782c04abc53c91aec22750ab988fc620
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed

diff -r d0250d01782c -r df053507edba Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/FSet.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -22,9 +22,9 @@
   apply(auto intro: list_eq.intros list_eq_refl)
   done
 
-quotient fset = "'a list" / "list_eq"
-  apply(rule equivp_list_eq)
-  done
+quotient_type 
+  fset = "'a list" / "list_eq"
+  by (rule equivp_list_eq)
 
 quotient_def
    "EMPTY :: 'a fset"
@@ -271,7 +271,7 @@
 apply (lifting list_induct_part)
 done
 
-quotient fset2 = "'a list" / "list_eq"
+quotient_type fset2 = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
 quotient_def
diff -r d0250d01782c -r df053507edba Quot/Examples/FSet2.thy
--- a/Quot/Examples/FSet2.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/FSet2.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -21,7 +21,7 @@
 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 by (auto intro: list_eq.intros list_eq_refl)
 
-quotient fset = "'a list" / "list_eq"
+quotient_type fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
 quotient_def
diff -r d0250d01782c -r df053507edba Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -12,7 +12,7 @@
 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 by auto
 
-quotient fset = "'a list" / "list_eq"
+quotient_type fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
 lemma not_nil_equiv_cons: 
diff -r d0250d01782c -r df053507edba Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -7,7 +7,7 @@
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
-quotient my_int = "nat \<times> nat" / intrel
+quotient_type my_int = "nat \<times> nat" / intrel
   apply(unfold equivp_def)
   apply(auto simp add: mem_def expand_fun_eq)
   done
diff -r d0250d01782c -r df053507edba Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -11,7 +11,7 @@
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
-quotient int = "nat \<times> nat" / intrel
+quotient_type int = "nat \<times> nat" / intrel
   unfolding equivp_def
   by (auto simp add: mem_def expand_fun_eq)
 
diff -r d0250d01782c -r df053507edba Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/LFex.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -73,11 +73,12 @@
   and   "equivp atrm"
 sorry
 
-quotient KIND = kind / akind
+quotient_type KIND = kind / akind
   by (rule alpha_equivps)
 
-quotient TY = ty / aty
-   and   TRM = trm / atrm
+quotient_type 
+    TY = ty / aty and   
+    TRM = trm / atrm
   by (auto intro: alpha_equivps)
 
 quotient_def
diff -r d0250d01782c -r df053507edba Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -50,7 +50,7 @@
   shows "equivp alpha"
 sorry
 
-quotient lam = rlam / alpha
+quotient_type lam = rlam / alpha
   apply(rule alpha_equivp)
   done
 
diff -r d0250d01782c -r df053507edba Quot/Examples/LarryDatatype.thy
--- a/Quot/Examples/LarryDatatype.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -121,7 +121,7 @@
 
 subsection{*The Initial Algebra: A Quotiented Message Type*}
 
-quotient  msg = freemsg / msgrel
+quotient_type msg = freemsg / msgrel
   by (rule equiv_msgrel)
 
 text{*The abstract message constructors*}
diff -r d0250d01782c -r df053507edba Quot/Examples/LarryInt.thy
--- a/Quot/Examples/LarryInt.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/LarryInt.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -10,7 +10,7 @@
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
-quotient int = "nat \<times> nat" / intrel
+quotient_type int = "nat \<times> nat" / intrel
   by (auto simp add: equivp_def expand_fun_eq)
 
 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
diff -r d0250d01782c -r df053507edba Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/quotient_typ.ML	Sun Dec 20 00:26:53 2009 +0100
@@ -219,8 +219,8 @@
 val _ = OuterKeyword.keyword "/"
 
 val _ = 
-    OuterSyntax.local_theory_to_proof "quotient" 
-      "quotient type definitions (requires equivalence proofs)"
+    OuterSyntax.local_theory_to_proof "quotient_type" 
+      "quotient type definitions (require equivalence proofs)"
          OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)
diff -r d0250d01782c -r df053507edba isar-keywords-quot.el
--- a/isar-keywords-quot.el	Sun Dec 20 00:15:40 2009 +0100
+++ b/isar-keywords-quot.el	Sun Dec 20 00:26:53 2009 +0100
@@ -193,8 +193,8 @@
     "quickcheck"
     "quickcheck_params"
     "quit"
-    "quotient"
     "quotient_def"
+    "quotient_type"
     "realizability"
     "realizers"
     "recdef"
@@ -511,7 +511,7 @@
     "nominal_inductive2"
     "nominal_primrec"
     "prove"
-    "quotient"
+    "quotient_type"
     "recdef_tc"
     "rep_datatype"
     "specification"