diff -r f04b33ce250f -r a4dc62a46ee4 IOA/meta_theory/Asig.thy --- a/IOA/meta_theory/Asig.thy Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,45 +0,0 @@ -(* Title: HOL/IOA/meta_theory/Asig.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -Action signatures -*) - -Asig = Option + - -types - -'a signature = "('a set * 'a set * 'a set)" - -consts - actions,inputs,outputs,internals,externals - ::"'action signature => 'action set" - is_asig ::"'action signature => bool" - mk_ext_asig ::"'action signature => 'action signature" - - -defs - -asig_inputs_def "inputs == fst" -asig_outputs_def "outputs == (fst o snd)" -asig_internals_def "internals == (snd o snd)" - -actions_def - "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" - -externals_def - "externals(asig) == (inputs(asig) Un outputs(asig))" - -is_asig_def - "is_asig(triple) == - ((inputs(triple) Int outputs(triple) = {}) & - (outputs(triple) Int internals(triple) = {}) & - (inputs(triple) Int internals(triple) = {}))" - - -mk_ext_asig_def - "mk_ext_asig(triple) == " - - -end