isabelle: src/HOL/IOA/ABP/Action.ML@3ae9fe3c0f68 (annotated)

1138 82fd99d5a6ff polish mueller parents: 1050 diff changeset	1	(* Title: HOL/IOA/example/Action.ML
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	2	ID: $Id$
1138 82fd99d5a6ff polish mueller parents: 1050 diff changeset	3	Author: Tobias Nipkow & Konrad Slind
82fd99d5a6ff polish mueller parents: 1050 diff changeset	4	Copyright 1994 TU Muenchen
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	5
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	6	Derived rules for actions
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	7	*)
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	8
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	9	goal Action.thy "!!x. x = y ==> action_case a b c d e f g x = \
0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	10	\ action_case a b c d e f g y";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1138 diff changeset	11	by (Asm_simp_tac 1);
1050 0c36c6a52a1d ABP: Alternating bit protocol example nipkow parents: diff changeset	12
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1138 diff changeset	13	Addcongs [result()];