IOA/example/Action.ML

--- a/IOA/example/Action.ML	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  Title:      HOL/IOA/example/Action.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow & Konrad Slind
-    Copyright   1994  TU Muenchen
-
-Derived rules for actions
-*)
-
-goal Action.thy "!!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 HOL_ss 1);
-
-val action_ss = arith_ss addcongs [result()] addsimps Action.action.simps;