diff -r 04412cfe6861 -r 2de17c994071 src/HOLCF/IOA/meta_theory/Asig.thy --- a/src/HOLCF/IOA/meta_theory/Asig.thy Mon Jun 09 10:21:38 1997 +0200 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy Thu Jun 12 16:47:15 1997 +0200 @@ -13,7 +13,7 @@ 'a signature = "('a set * 'a set * 'a set)" consts - actions,inputs,outputs,internals,externals + actions,inputs,outputs,internals,externals,locals ::"'action signature => 'action set" is_asig ::"'action signature => bool" mk_ext_asig ::"'action signature => 'action signature" @@ -31,6 +31,9 @@ externals_def "externals(asig) == (inputs(asig) Un outputs(asig))" +locals_def + "locals asig == ((internals asig) Un (outputs asig))" + is_asig_def "is_asig(triple) == ((inputs(triple) Int outputs(triple) = {}) &