# HG changeset patch
# User wenzelm
# Date 1125758743 -7200
# Node ID b1cf9189104e29617afe6960c5ec0e277f4f2280
# Parent  75407a6f02d25e5d36067c0c8e6dcd9f1edbd18f
removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;

diff -r 75407a6f02d2 -r b1cf9189104e src/HOLCF/IOA/Storage/Action.ML
--- a/src/HOLCF/IOA/Storage/Action.ML	Sat Sep 03 16:44:17 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(*  Title:      HOLCF/IOA/ABP/Action.ML
-    ID:         $Id$
-    Author:     Olaf Müller
-
-Derived rules for actions.
-*)
-
-Goal "!!x. x = y ==> action_case a b c x =     \
-\                        action_case a b c y";
-by (Asm_simp_tac 1);
-
-Addcongs [result()];
diff -r 75407a6f02d2 -r b1cf9189104e src/HOLCF/IOA/Storage/Impl.ML
--- a/src/HOLCF/IOA/Storage/Impl.ML	Sat Sep 03 16:44:17 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      HOL/IOA/example/Sender.thy
-    ID:         $Id$
-    Author:     Olaf Müller
-
-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";
diff -r 75407a6f02d2 -r b1cf9189104e src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sat Sep 03 16:44:17 2005 +0200
+++ b/src/HOLCF/IsaMakefile	Sat Sep 03 16:45:43 2005 +0200
@@ -146,9 +146,8 @@
 
 IOA-Storage: IOA $(LOG)/IOA-Storage.gz
 
-$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.ML \
-  IOA/Storage/Action.thy IOA/Storage/Correctness.ML \
-  IOA/Storage/Correctness.thy IOA/Storage/Impl.ML IOA/Storage/Impl.thy \
+$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy IOA/Storage/Correctness.ML \
+  IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \
   IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage