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
oheimb@4530
     1
(*  Title:      HOL/IOA/Asig.ML
mueller@3078
     2
    ID:         $Id$
mueller@3078
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@3078
     4
    Copyright   1994  TU Muenchen
mueller@3078
     5
mueller@3078
     6
Action signatures
mueller@3078
     7
*)
mueller@3078
     8
mueller@3078
     9
open Asig;
mueller@3078
    10
mueller@3078
    11
val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
mueller@3078
    12
paulson@5143
    13
Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
wenzelm@4089
    14
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
mueller@3078
    15
qed"int_and_ext_is_act";
mueller@3078
    16
paulson@5143
    17
Goal "[|a:externals(S)|] ==> a:actions(S)";
wenzelm@4089
    18
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1);
mueller@3078
    19
qed"ext_is_act";