isabelle: src/HOLCF/IOA/Storage/Impl.ML@0a68dc9edba5 (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	wenzelm
	Fri, 10 Nov 2000 19:11:51 +0100
changeset 10443	0a68dc9edba5
parent 7322	d16d7ddcc842
child 12218	6597093b77e7
permissions	-rw-r--r--