--- a/src/HOLCF/IOA/ABP/Action.ML Tue Mar 28 17:32:24 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: HOLCF/IOA/ABP/Action.ML
- ID: $Id$
- Author: Olaf Mueller
- Copyright 1995 TU Muenchen
-
-Derived rules for actions
-*)
-
-Goal "!!x. x = y ==> action_case a b c d e f g x = \
-\ action_case a b c d e f g y";
-by (Asm_simp_tac 1);
-
-Addcongs [result()];
--- a/src/HOLCF/IOA/NTP/Action.ML Tue Mar 28 17:32:24 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: HOL/IOA/NTP/Action.ML
- ID: $Id$
- Author: Tobias Nipkow & Konrad Slind
- Copyright 1994 TU Muenchen
-
-Derived rules for actions
-*)
-
-Goal "!!x. x = y ==> action_case a b c d e f g h i j x = \
-\ action_case a b c d e f g h i j y";
-by (Asm_simp_tac 1);
-
-Addcongs [result()];
--- a/src/HOLCF/IsaMakefile Tue Mar 28 17:32:24 2000 +0200
+++ b/src/HOLCF/IsaMakefile Tue Mar 28 17:33:44 2000 +0200
@@ -95,7 +95,7 @@
IOA-ABP: IOA $(LOG)/IOA-ABP.gz
$(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \
- IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML IOA/ABP/Action.thy \
+ IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \
IOA/ABP/Check.ML IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \
IOA/ABP/Lemmas.ML IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
@@ -108,7 +108,7 @@
IOA-NTP: IOA $(LOG)/IOA-NTP.gz
$(LOG)/IOA-NTP.gz: $(OUT)/IOA IOA/NTP/Abschannel.ML \
- IOA/NTP/Abschannel.thy IOA/NTP/Action.ML IOA/NTP/Action.thy \
+ IOA/NTP/Abschannel.thy IOA/NTP/Action.thy \
IOA/NTP/Correctness.ML IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML IOA/NTP/Lemmas.thy \
IOA/NTP/Multiset.ML IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \