--- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Tue Apr 18 00:36:02 2000 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Tue Apr 18 00:49:49 2000 +0200
@@ -29,7 +29,7 @@
pre "(a=PonR --> APonR_incl) & (a=None --> ~APonR_incl)"
post info:="None",APonR_incl:="if (a=PonR) then False else APonR_incl"
-automaton cockpit_hide = hide "Info a" in cockpit
+automaton cockpit_hide = hide_action "Info a" in cockpit
(*Subsequent automata express the properties to be proved, see also
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Apr 18 00:36:02 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Apr 18 00:49:49 2000 +0200
@@ -552,7 +552,7 @@
(Scan.optional initial "True") --
translist))))) >> mk_ioa_decl ||
(P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "hide" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name))))
+ (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name))))
>> mk_hiding_decl ||
(P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term))))
>> mk_restriction_decl ||
@@ -570,7 +570,7 @@
val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
"outputs", "internals", "states", "initially", "transitions", "pre",
- "post", "transrel", ":=", "compose", "hide", "in", "restrict", "to",
+ "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
"rename", "using"];
val _ = OuterSyntax.add_parsers [automatonP];
--- a/src/HOLCF/IOA/meta_theory/ioa_syn.ML Tue Apr 18 00:36:02 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_syn.ML Tue Apr 18 00:49:49 2000 +0200
@@ -143,7 +143,7 @@
("compose" $$-- (enum1 "," name))) >> mk_composition_decl)
||
(name -- ("=" $$--
- ("hide" $$-- (enum1 "," string) --
+ ("hide_action" $$-- (enum1 "," string) --
("in" $$-- name))) >> mk_hiding_decl)
||
(name -- ("=" $$--
@@ -164,7 +164,7 @@
val _ = ThySyn.add_syntax
["signature","actions","inputs", "outputs", "internals", "states", "initially",
"transitions", "pre", "post", "transrel",":=",
-"compose","hide","in","restrict","to","rename","using"]
+"compose","hide_action","in","restrict","to","rename","using"]
[axm_section "automaton" "" ioa_decl];
end;