author | wenzelm |
Thu, 15 Nov 2001 23:25:46 +0100 | |
changeset 12218 | 6597093b77e7 |
parent 7322 | d16d7ddcc842 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
6008 | 1 |
(* Title: HOL/IOA/example/Sender.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6008 | 5 |
|
12218 | 6 |
Impl. |
6008 | 7 |
*) |
8 |
||
9 |
Goal |
|
10 |
"New : actions(impl_sig) & \ |
|
11 |
\ Loc l : actions(impl_sig) & \ |
|
12 |
\ Free l : actions(impl_sig) "; |
|
7322 | 13 |
by (simp_tac (simpset() addsimps |
6008 | 14 |
(Impl.sig_def :: actions_def :: |
15 |
asig_projections)) 1); |
|
16 |
qed "in_impl_asig"; |