changeset 3072 | a31419014be5 |
child 5068 | fb28eaa07e01 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/ABP/Action.ML Wed Apr 30 11:24:14 1997 +0200 @@ -0,0 +1,13 @@ +(* Title: HOLCF/IOA/ABP/Action.ML + ID: $Id$ + Author: 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 1); + +Addcongs [result()];