--- a/src/HOL/IOA/Asig.thy Tue Sep 06 18:49:25 2005 +0200
+++ b/src/HOL/IOA/Asig.thy Tue Sep 06 19:03:39 2005 +0200
@@ -2,44 +2,50 @@
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
-
-Action signatures
*)
-Asig = Main +
+header {* Action signatures *}
-types
+theory Asig
+imports Main
+begin
-'a signature = "('a set * 'a set * 'a set)"
+types
+ 'a signature = "('a set * 'a set * 'a set)"
consts
- actions,inputs,outputs,internals,externals
- ::"'action signature => 'action set"
+ "actions" :: "'action signature => 'action set"
+ "inputs" :: "'action signature => 'action set"
+ "outputs" :: "'action signature => 'action set"
+ "internals" :: "'action signature => 'action set"
+ 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)"
+asig_inputs_def: "inputs == fst"
+asig_outputs_def: "outputs == (fst o snd)"
+asig_internals_def: "internals == (snd o snd)"
-actions_def
+actions_def:
"actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
-externals_def
+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) = {}) &
+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_def:
"mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
+ML {* use_legacy_bindings (the_context ()) *}
-end
+end