# HG changeset patch # User wenzelm # Date 956011789 -7200 # Node ID 3213613a775a0b1edf4bb99b14b43b42920504a8 # Parent aef229ca5e77aebf67ea02540a4cdb0f9a992dfa renamed 'hide' to 'hide_action'; diff -r aef229ca5e77 -r 3213613a775a src/HOLCF/IOA/Modelcheck/Cockpit.thy --- 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 diff -r aef229ca5e77 -r 3213613a775a src/HOLCF/IOA/meta_theory/ioa_package.ML --- 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]; diff -r aef229ca5e77 -r 3213613a775a src/HOLCF/IOA/meta_theory/ioa_syn.ML --- 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;