equal
deleted
inserted
replaced
1 (* Title: HOL/IOA/Asig.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 *) |
|
6 |
|
7 bind_thms ("asig_projections", [asig_inputs_def, asig_outputs_def, asig_internals_def]); |
|
8 |
|
9 Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"; |
|
10 by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); |
|
11 qed"int_and_ext_is_act"; |
|
12 |
|
13 Goal "[|a:externals(S)|] ==> a:actions(S)"; |
|
14 by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); |
|
15 qed"ext_is_act"; |
|