src/HOLCF/IOA/Storage/Impl.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/Storage/Impl.ML	Wed Dec 02 15:55:39 1998 +0100
@@ -0,0 +1,16 @@
+(*  Title:      HOL/IOA/example/Sender.thy
+    ID:         $Id$
+    Author:     Olaf Mueller
+    Copyright   1997  TU Muenchen
+
+Impl
+*)
+ 
+Goal 
+ "New : actions(impl_sig)       &   \
+\ Loc l : actions(impl_sig)       &   \
+\ Free l : actions(impl_sig) ";
+by(simp_tac (simpset() addsimps 
+             (Impl.sig_def :: actions_def :: 
+              asig_projections)) 1);
+qed "in_impl_asig";