src/HOLCF/IOA/meta_theory/ioa_package.ML
changeset 8733 3213613a775a
parent 8438 b8389b4fca9c
child 9317 7a72952ca068
     1.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Apr 18 00:36:02 2000 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Apr 18 00:49:49 2000 +0200
     1.3 @@ -552,7 +552,7 @@
     1.4            (Scan.optional initial "True") --
     1.5          translist))))) >> mk_ioa_decl ||
     1.6    (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl ||
     1.7 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name))))
     1.8 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name))))
     1.9      >> mk_hiding_decl ||
    1.10    (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term))))
    1.11      >> mk_restriction_decl ||
    1.12 @@ -570,7 +570,7 @@
    1.13  
    1.14  val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
    1.15    "outputs", "internals", "states", "initially", "transitions", "pre",
    1.16 -  "post", "transrel", ":=", "compose", "hide", "in", "restrict", "to",
    1.17 +  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
    1.18    "rename", "using"];
    1.19  
    1.20  val _ = OuterSyntax.add_parsers [automatonP];