# HG changeset patch
# User nipkow
# Date 954257624 -7200
# Node ID f077613e8e7bfc231f45efb194b40820be5e8893
# Parent  8fb3a81b4ccfaf9b893a03338e10ac40db5c0d97
mods because of weak_case_cong -> removed Action.ML twice

diff -r 8fb3a81b4ccf -r f077613e8e7b src/HOLCF/IOA/ABP/Action.ML
--- 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()];
diff -r 8fb3a81b4ccf -r f077613e8e7b src/HOLCF/IOA/NTP/Action.ML
--- 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()];
diff -r 8fb3a81b4ccf -r f077613e8e7b src/HOLCF/IsaMakefile
--- 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 \