src/HOL/IOA/Asig.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 5143 b94cd208f073
child 17288 aa3833fb7bee
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/IOA/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 "[| 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 "[|a:externals(S)|] ==> a:actions(S)";
    18 by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
    19 qed"ext_is_act";