--- a/QuotMain.thy	Mon Oct 12 22:44:16 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 23:06:14 2009 +0200
@@ -3,7 +3,6 @@
 uses ("quotient.ML")
 begin
 
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -143,9 +142,24 @@
 end
 
 section {* type definition for the quotient type *}
+ML {* Binding.name *}
+
+ML {* cat_lines *}
 
 use "quotient.ML"
 
+ML {*
+  mk_typedef;
+  mk_typedef_cmd;
+  quottype_parser
+*}
+
+ML {* Proof.theorem_i *}
+
+term EQUIV
+
+ML {* quottype_parser *}
+ML {* OuterSyntax.local_theory_to_proof *}
 
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -166,16 +180,24 @@
 where
   r_eq: "EQUIV RR"
 
+quotient qtrm = "trm" / "RR"
+  apply(rule r_eq)
+  done
+
+(*
 local_setup {*
   typedef_main (@{binding "qtrm"}, NoSyn, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
 *}
+*)
 
+typ qtrm
 term Rep_qtrm
 term REP_qtrm
 term Abs_qtrm
 term ABS_qtrm
 thm QUOT_TYPE_qtrm
 thm QUOTIENT_qtrm
+thm REP_qtrm_def
 
 (* Test interpretation *)
 thm QUOT_TYPE_I_qtrm.thm11
@@ -194,10 +216,15 @@
 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 
-
+(*
 local_setup {*
   typedef_main (@{binding "qtrm'"}, NoSyn, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
 *}
+*)
+
+quotient "'a qtrm'" = "'a trm'" / "R'"
+  apply(rule r_eq')
+  done
 
 print_theorems
 
@@ -217,9 +244,14 @@
 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
 axioms t_eq: "EQUIV Rt"
 
+(*
 local_setup {*
   typedef_main (@{binding "qt"}, NoSyn, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
 *}
+*)
+
+quotient "qt" = "t" / "Rt"
+  by (rule t_eq)
 
 section {* lifting of constants *}
 
@@ -381,7 +413,7 @@
   val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
   val def_trm = get_const_def nconst oconst rty qty lthy
 in
-  make_def (nconst_bname, mx, def_trm) lthy
+  define (nconst_bname, mx, def_trm) lthy
 end
 *}
 
@@ -408,10 +440,15 @@
 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 axioms t_eq': "EQUIV Rt'"
 
-
+(*
 local_setup {*
   typedef_main (@{binding "qt'"}, NoSyn, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
 *}
+*)
+
+quotient "'a qt'" = "'a t'" / "Rt'"
+  apply(rule t_eq')
+  done
 
 print_theorems
 
@@ -454,9 +491,15 @@
   apply(auto intro: list_eq.intros list_eq_refl)
   done
 
+(*
 local_setup {*
   typedef_main (@{binding "fset"}, NoSyn, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
 *}
+*)
+
+quotient "'a fset" = "'a list" / "list_eq"
+  apply(rule equiv_list_eq)
+  done
 
 print_theorems