# HG changeset patch # User haftmann # Date 1167420857 -3600 # Node ID 56abe5f3c612a0886e959ec9030e014cde1b0bee # Parent e97fd6480091b909bb8942d1ba59fa6e94a723ce changed syntax for axclass attach diff -r e97fd6480091 -r 56abe5f3c612 src/HOL/Code_Generator.thy --- a/src/HOL/Code_Generator.thy Fri Dec 29 19:50:52 2006 +0100 +++ b/src/HOL/Code_Generator.thy Fri Dec 29 20:34:17 2006 +0100 @@ -83,7 +83,7 @@ text {* operational equality for code generation *} axclass eq \ type - attach "op =" + (attach "op =") text {* equality for Haskell *} diff -r e97fd6480091 -r 56abe5f3c612 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Dec 29 19:50:52 2006 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Dec 29 20:34:17 2006 +0100 @@ -88,7 +88,7 @@ OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl (P.name -- Scan.optional ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! (P.list1 P.xname)) [] - -- Scan.optional (P.$$$ "attach" |-- Scan.repeat P.term) [] + -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] -- Scan.repeat (P.thm_name ":" -- (P.prop >> single)) >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));