src/HOLCF/IOA/meta_theory/ioa_package.ML
changeset 8733 3213613a775a
parent 8438 b8389b4fca9c
child 9317 7a72952ca068
equal deleted inserted replaced
8732:aef229ca5e77 8733:3213613a775a
   550           (Scan.optional internalslist []) --
   550           (Scan.optional internalslist []) --
   551           stateslist --
   551           stateslist --
   552           (Scan.optional initial "True") --
   552           (Scan.optional initial "True") --
   553         translist))))) >> mk_ioa_decl ||
   553         translist))))) >> mk_ioa_decl ||
   554   (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl ||
   554   (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl ||
   555   (P.name -- (P.$$$ "=" |-- (P.$$$ "hide" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name))))
   555   (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name))))
   556     >> mk_hiding_decl ||
   556     >> mk_hiding_decl ||
   557   (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term))))
   557   (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term))))
   558     >> mk_restriction_decl ||
   558     >> mk_restriction_decl ||
   559   (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "using" |-- P.term))))
   559   (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "using" |-- P.term))))
   560     >> mk_rename_decl;
   560     >> mk_rename_decl;
   568 
   568 
   569 (* setup outer syntax *)
   569 (* setup outer syntax *)
   570 
   570 
   571 val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
   571 val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
   572   "outputs", "internals", "states", "initially", "transitions", "pre",
   572   "outputs", "internals", "states", "initially", "transitions", "pre",
   573   "post", "transrel", ":=", "compose", "hide", "in", "restrict", "to",
   573   "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   574   "rename", "using"];
   574   "rename", "using"];
   575 
   575 
   576 val _ = OuterSyntax.add_parsers [automatonP];
   576 val _ = OuterSyntax.add_parsers [automatonP];
   577 
   577 
   578 
   578