isabelle: src/HOLCF/IOA/Storage/Impl.ML@851c90b23a9e (annotated)

6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	1	(* Title: HOL/IOA/example/Sender.thy
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	2	ID: $Id$
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	3	Author: Olaf Mueller
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	4	Copyright 1997 TU Muenchen
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	5
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	6	Impl
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
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	9	Goal
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	10	"New : actions(impl_sig) & \
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	11	\ Loc l : actions(impl_sig) & \
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	12	\ Free l : actions(impl_sig) ";
7322 d16d7ddcc842 isatool expandshort; wenzelm parents: 6008 diff changeset	13	by (simp_tac (simpset() addsimps
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	14	(Impl.sig_def :: actions_def ::
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	15	asig_projections)) 1);
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	16	qed "in_impl_asig";

author	paulson
	Mon, 05 Mar 2001 15:25:11 +0100
changeset 11193	851c90b23a9e
parent 7322	d16d7ddcc842
child 12218	6597093b77e7
permissions	-rw-r--r--