author | wenzelm |
Mon, 28 Jun 1999 23:02:38 +0200 | |
changeset 6853 | 80f88b762816 |
parent 6008 | d0e9b1619468 |
child 7322 | d16d7ddcc842 |
permissions | -rw-r--r-- |
6008 | 1 |
(* Title: HOL/IOA/example/Sender.thy |
2 |
ID: $Id$ |
|
3 |
Author: Olaf Mueller |
|
4 |
Copyright 1997 TU Muenchen |
|
5 |
||
6 |
Impl |
|
7 |
*) |
|
8 |
||
9 |
Goal |
|
10 |
"New : actions(impl_sig) & \ |
|
11 |
\ Loc l : actions(impl_sig) & \ |
|
12 |
\ Free l : actions(impl_sig) "; |
|
13 |
by(simp_tac (simpset() addsimps |
|
14 |
(Impl.sig_def :: actions_def :: |
|
15 |
asig_projections)) 1); |
|
16 |
qed "in_impl_asig"; |