# HG changeset patch
# User haftmann
# Date 1164187277 -3600
# Node ID 74ddf3a522f831d1bb7b02075f823a82570b5a15
# Parent  51239d45247bc143d6f9f0b2cd87004b52ebe397
added Isar syntax for adding parameters to axclasses

diff -r 51239d45247b -r 74ddf3a522f8 NEWS
--- 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
diff -r 51239d45247b -r 74ddf3a522f8 src/Pure/Isar/isar_syn.ML
--- 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",