--- a/src/Pure/Isar/isar_syn.ML Mon Dec 03 16:04:16 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Dec 03 16:04:17 2007 +0100
@@ -445,7 +445,7 @@
Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class)));
val _ =
- OuterSyntax.command "instantiation" "prove type arity" K.thy_decl
+ OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
(P.and_list1 P.arity --| P.begin
>> (fn arities => Toplevel.print o
Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
@@ -459,6 +459,17 @@
|| Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
+(* arbitrary overloading *)
+
+val _ =
+ OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
+ (Scan.repeat1 (P.xname --| P.$$$ "::" -- P.typ --| P.$$$ "is" -- P.name --
+ Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true)
+ --| P.begin
+ >> (fn operations => Toplevel.print o
+ Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));
+
+
(* code generation *)
val _ =