isabelle: src/HOL/IOA/NTP/Action.ML@23ceb1dc9755 (annotated)

1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	1	(* Title: HOL/IOA/NTP/Action.ML
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	2	ID: $Id$
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	4	Copyright 1994 TU Muenchen
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	5
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	6	Derived rules for actions
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	7	*)
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	8
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	9	goal Action.thy "!!x. x = y ==> action_case a b c d e f g h i j x = \
4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	10	\ action_case a b c d e f g h i j y";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1051 diff changeset	11	by (Asm_simp_tac 1);
1051 4fcd0638e61d Directory example is now called NTP nipkow parents: diff changeset	12
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1051 diff changeset	13	Addcongs [result()];