src/HOL/IOA/meta_theory/Asig.ML
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1465 5d7a7e439cec
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
     1 (*  Title:      HOL/IOA/meta_theory/Asig.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 
     6 Action signatures
     7 *)
     8 
     9 open Asig;
    10 
    11 val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
    12 
    13 goal Asig.thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
    14 by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
    15 qed"int_and_ext_is_act";
    16 
    17 goal Asig.thy "!!a.[|a:externals(S)|] ==> a:actions(S)";
    18 by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
    19 qed"ext_is_act";