author | wenzelm |
Thu, 15 Nov 2001 23:25:46 +0100 | |
changeset 12218 | 6597093b77e7 |
parent 6008 | d0e9b1619468 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
6008 | 1 |
(* Title: HOLCF/IOA/ABP/Action.ML |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6008 | 5 |
|
12218 | 6 |
Derived rules for actions. |
6008 | 7 |
*) |
8 |
||
9 |
Goal "!!x. x = y ==> action_case a b c x = \ |
|
10 |
\ action_case a b c y"; |
|
11 |
by (Asm_simp_tac 1); |
|
12 |
||
13 |
Addcongs [result()]; |