--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Feb 24 21:45:11 2002 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Feb 24 21:45:57 2002 +0100
@@ -522,7 +522,7 @@
>> mk_hiding_decl ||
(P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term))))
>> mk_restriction_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "using" |-- P.term))))
+ (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "to" |-- P.term))))
>> mk_rename_decl;
val automatonP =
@@ -537,7 +537,7 @@
val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
"outputs", "internals", "states", "initially", "transitions", "pre",
"post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
- "rename", "using"];
+ "rename"];
val _ = OuterSyntax.add_parsers [automatonP];
--- a/src/HOLCF/IOA/meta_theory/ioa_syn.ML Sun Feb 24 21:45:11 2002 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_syn.ML Sun Feb 24 21:45:57 2002 +0100
@@ -151,7 +151,7 @@
("to" $$-- (enum1 "," string)))) >> mk_restriction_decl)
||
(name -- ("=" $$--
- ("rename" $$-- name -- ("using" $$-- string))) >> mk_rename_decl)
+ ("rename" $$-- name -- ("to" $$-- string))) >> mk_rename_decl)
;
in
@@ -164,7 +164,7 @@
val _ = ThySyn.add_syntax
["signature","actions","inputs", "outputs", "internals", "states", "initially",
"transitions", "pre", "post", "transrel",":=",
-"compose","hide_action","in","restrict","to","rename","using"]
+"compose","hide_action","in","restrict","to","rename"]
[axm_section "automaton" "" ioa_decl];
end;