--- a/NEWS Wed Nov 22 10:20:22 2006 +0100
+++ b/NEWS Wed Nov 22 10:21:17 2006 +0100
@@ -560,7 +560,7 @@
INCOMPATIBILITY: ML code directly refering to constant names may need adaption
This in general only affects hand-written proof tactics, simprocs and so on.
-* New theory Code_Generator providing class 'eq' with constant 'eq',
+* New theory Code_Generator providing class 'eq',
allowing for code generation with polymorphic equality.
* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
--- a/src/Pure/Isar/isar_syn.ML Wed Nov 22 10:20:22 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Nov 22 10:21:17 2006 +0100
@@ -86,10 +86,11 @@
val axclassP =
OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
- ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
- P.!!! (P.list1 P.xname)) []) --
- Scan.repeat (P.thm_name ":" -- (P.prop >> single))
- >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
+ (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
+ P.!!! (P.list1 P.xname)) []
+ -- Scan.optional (P.$$$ "attach" |-- Scan.repeat P.term) []
+ -- Scan.repeat (P.thm_name ":" -- (P.prop >> single))
+ >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
(* types *)
@@ -887,7 +888,7 @@
val _ = OuterSyntax.add_keywords
["!", "!!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
- "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
+ "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "attach",
"begin", "binder", "concl", "constrains", "defines", "fixes", "for",
"imports", "if", "in", "includes", "infix", "infixl", "infixr",
"is", "notes", "obtains", "open", "output", "overloaded", "shows",