author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 12218 | 6597093b77e7 |
permissions | -rw-r--r-- |
6008 | 1 |
(* Title: HOL/IOA/example/Sender.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
6008 | 4 |
|
12218 | 5 |
Impl. |
6008 | 6 |
*) |
7 |
||
8 |
Goal |
|
9 |
"New : actions(impl_sig) & \ |
|
10 |
\ Loc l : actions(impl_sig) & \ |
|
11 |
\ Free l : actions(impl_sig) "; |
|
7322 | 12 |
by (simp_tac (simpset() addsimps |
6008 | 13 |
(Impl.sig_def :: actions_def :: |
14 |
asig_projections)) 1); |
|
15 |
qed "in_impl_asig"; |