isabelle: src/HOLCF/IOA/Storage/Action.ML@5b57f995a179 (annotated)

6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	1	(* Title: HOLCF/IOA/ABP/Action.ML
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 6008 diff changeset	3	Author: Olaf M�ller
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	4
12218 6597093b77e7 GPLed; wenzelm parents: 6008 diff changeset	5	Derived rules for actions.
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	6	*)
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	7
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	8	Goal "!!x. x = y ==> action_case a b c x = \
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	9	\ action_case a b c y";
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	10	by (Asm_simp_tac 1);
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	11
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	12	Addcongs [result()];