changed syntax for axclass attach
authorhaftmann
Fri Dec 29 20:34:17 2006 +0100 (2006-12-29 ago)
changeset 2195156abe5f3c612
parent 21950 e97fd6480091
child 21952 dc9366853df1
changed syntax for axclass attach
src/HOL/Code_Generator.thy
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/HOL/Code_Generator.thy	Fri Dec 29 19:50:52 2006 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Fri Dec 29 20:34:17 2006 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  text {* operational equality for code generation *}
     1.5  
     1.6  axclass eq \<subseteq> type
     1.7 -  attach "op ="
     1.8 +  (attach "op =")
     1.9  
    1.10  
    1.11  text {* equality for Haskell *}
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Dec 29 19:50:52 2006 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 29 20:34:17 2006 +0100
     2.3 @@ -88,7 +88,7 @@
     2.4    OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     2.5      (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
     2.6          P.!!! (P.list1 P.xname)) []
     2.7 -        -- Scan.optional (P.$$$ "attach" |-- Scan.repeat P.term) []
     2.8 +        -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
     2.9          -- Scan.repeat (P.thm_name ":" -- (P.prop >> single))
    2.10        >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
    2.11