--- a/quotient.ML Mon Oct 12 13:58:31 2009 +0200
+++ b/quotient.ML Mon Oct 12 14:30:50 2009 +0200
@@ -162,6 +162,26 @@
in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
end
+(* syntax setup *)
+local structure P = OuterParse in
+
+val quottype_parser =
+ (P.type_args -- P.binding) --
+ P.opt_infix --
+ (P.$$$ "=" |-- P.term) --
+ (P.$$$ "/" |-- P.term)
+
+(*
+val _ =
+ OuterSyntax.command "quotient" "quotient type definition (requires equivalence proof)"
+ OuterKeyword.thy_goal
+ (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
+
+end;
+*)
+
+end;
+
end;
open Quotient
\ No newline at end of file