| author | paulson |
| Wed, 28 Jun 2000 10:56:01 +0200 | |
| changeset 9172 | 2dbb80d4fdb7 |
| parent 7322 | d16d7ddcc842 |
| child 12218 | 6597093b77e7 |
| permissions | -rw-r--r-- |
(* Title: HOL/IOA/example/Sender.thy ID: $Id$ Author: Olaf Mueller Copyright 1997 TU Muenchen Impl *) Goal "New : actions(impl_sig) & \ \ Loc l : actions(impl_sig) & \ \ Free l : actions(impl_sig) "; by (simp_tac (simpset() addsimps (Impl.sig_def :: actions_def :: asig_projections)) 1); qed "in_impl_asig";