added Isar syntax for adding parameters to axclasses
authorhaftmann
Wed Nov 22 10:21:17 2006 +0100 (2006-11-22)
changeset 2146274ddf3a522f8
parent 21461 51239d45247b
child 21463 42dd50268c8b
added Isar syntax for adding parameters to axclasses
NEWS
src/Pure/Isar/isar_syn.ML
     1.1 --- a/NEWS	Wed Nov 22 10:20:22 2006 +0100
     1.2 +++ b/NEWS	Wed Nov 22 10:21:17 2006 +0100
     1.3 @@ -560,7 +560,7 @@
     1.4  INCOMPATIBILITY: ML code directly refering to constant names may need adaption
     1.5  This in general only affects hand-written proof tactics, simprocs and so on.
     1.6  
     1.7 -* New theory Code_Generator providing class 'eq' with constant 'eq',
     1.8 +* New theory Code_Generator providing class 'eq',
     1.9  allowing for code generation with polymorphic equality.
    1.10  
    1.11  * Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Nov 22 10:20:22 2006 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 22 10:21:17 2006 +0100
     2.3 @@ -86,10 +86,11 @@
     2.4  
     2.5  val axclassP =
     2.6    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     2.7 -    ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
     2.8 -        P.!!! (P.list1 P.xname)) []) --
     2.9 -          Scan.repeat (P.thm_name ":" -- (P.prop >> single))
    2.10 -      >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
    2.11 +    (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    2.12 +        P.!!! (P.list1 P.xname)) []
    2.13 +        -- Scan.optional (P.$$$ "attach" |-- Scan.repeat P.term) []
    2.14 +        -- Scan.repeat (P.thm_name ":" -- (P.prop >> single))
    2.15 +      >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
    2.16  
    2.17  
    2.18  (* types *)
    2.19 @@ -887,7 +888,7 @@
    2.20  
    2.21  val _ = OuterSyntax.add_keywords
    2.22   ["!", "!!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    2.23 -  "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
    2.24 +  "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "attach",
    2.25    "begin", "binder", "concl", "constrains", "defines", "fixes", "for",
    2.26    "imports", "if", "in", "includes", "infix", "infixl", "infixr",
    2.27    "is", "notes", "obtains", "open", "output", "overloaded", "shows",