diff -r 3e8d80cdd3e7 -r 750b766645b8 src/HOL/IOA/meta_theory/Asig.thy
--- a/src/HOL/IOA/meta_theory/Asig.thy	Wed Apr 30 11:53:30 1997 +0200
+++ /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 = Prod +
-
-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) == (inputs(triple), outputs(triple), {})"
-
-
-end