src/HOL/IOA/ABP/Action.ML
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1266 3ae9fe3c0f68
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
mueller@1138
     1
(*  Title:      HOL/IOA/example/Action.ML
nipkow@1050
     2
    ID:         $Id$
mueller@1138
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@1138
     4
    Copyright   1994  TU Muenchen
nipkow@1050
     5
nipkow@1050
     6
Derived rules for actions
nipkow@1050
     7
*)
nipkow@1050
     8
nipkow@1050
     9
goal Action.thy "!!x. x = y ==> action_case a b c d e f g x =     \
nipkow@1050
    10
\                               action_case a b c d e f g y";
clasohm@1266
    11
by (Asm_simp_tac 1);
nipkow@1050
    12
clasohm@1266
    13
Addcongs [result()];