| author | haftmann |
| Thu, 15 Sep 2005 08:16:22 +0200 | |
| changeset 17401 | 9147c880ada6 |
| parent 17288 | aa3833fb7bee |
| permissions | -rw-r--r-- |
| 4530 | 1 |
(* Title: HOL/IOA/Asig.ML |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow & Konrad Slind |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
4 |
Copyright 1994 TU Muenchen |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
5 |
*) |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
6 |
|
| 17288 | 7 |
bind_thms ("asig_projections", [asig_inputs_def, asig_outputs_def, asig_internals_def]);
|
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
8 |
|
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
9 |
Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"; |
| 4089 | 10 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
11 |
qed"int_and_ext_is_act"; |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
12 |
|
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
13 |
Goal "[|a:externals(S)|] ==> a:actions(S)"; |
| 4089 | 14 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
15 |
qed"ext_is_act"; |