changeset 6008 | d0e9b1619468 |
child 12218 | 6597093b77e7 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/Storage/Action.ML Wed Dec 02 15:55:39 1998 +0100 @@ -0,0 +1,13 @@ +(* Title: HOLCF/IOA/ABP/Action.ML + ID: $Id$ + Author: Olaf Mueller + Copyright 1997 TU Muenchen + +Derived rules for actions +*) + +Goal "!!x. x = y ==> action_case a b c x = \ +\ action_case a b c y"; +by (Asm_simp_tac 1); + +Addcongs [result()];