src/Pure/Isar/isar_syn.ML
changeset 21462 74ddf3a522f8
parent 21437 a3c55b85cf0e
child 21527 7140f8aba380
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Nov 22 10:20:22 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 22 10:21:17 2006 +0100
     1.3 @@ -86,10 +86,11 @@
     1.4  
     1.5  val axclassP =
     1.6    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     1.7 -    ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
     1.8 -        P.!!! (P.list1 P.xname)) []) --
     1.9 -          Scan.repeat (P.thm_name ":" -- (P.prop >> single))
    1.10 -      >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
    1.11 +    (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    1.12 +        P.!!! (P.list1 P.xname)) []
    1.13 +        -- Scan.optional (P.$$$ "attach" |-- Scan.repeat P.term) []
    1.14 +        -- Scan.repeat (P.thm_name ":" -- (P.prop >> single))
    1.15 +      >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
    1.16  
    1.17  
    1.18  (* types *)
    1.19 @@ -887,7 +888,7 @@
    1.20  
    1.21  val _ = OuterSyntax.add_keywords
    1.22   ["!", "!!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    1.23 -  "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
    1.24 +  "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "attach",
    1.25    "begin", "binder", "concl", "constrains", "defines", "fixes", "for",
    1.26    "imports", "if", "in", "includes", "infix", "infixl", "infixr",
    1.27    "is", "notes", "obtains", "open", "output", "overloaded", "shows",