changeset 1050 | 0c36c6a52a1d |
child 1138 | 82fd99d5a6ff |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/ABP/Action.ML Thu Apr 13 16:55:14 1995 +0200 @@ -0,0 +1,13 @@ +(* Title: HOL/IOA/ABP/Action.ML + ID: $Id$ + Author: Tobias Nipkow & Olaf Mueller + Copyright 1995 TU Muenchen + +Derived rules for actions +*) + +goal Action.thy "!!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 HOL_ss 1); + +val action_ss = arith_ss addcongs [result()] addsimps Action.action.simps;