diff -r 722bf1319be5 -r fd1be45b64bf IOA/example/Action.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Action.ML	Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,5 @@
+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;