equal
deleted
inserted
replaced
396 Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)"; |
396 Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)"; |
397 by (auto_tac (claset(), |
397 by (auto_tac (claset(), |
398 simpset() addsimps [constrains_def, project_set_def])); |
398 simpset() addsimps [constrains_def, project_set_def])); |
399 by (Force_tac 1); |
399 by (Force_tac 1); |
400 qed "extend_constrains_project_set"; |
400 qed "extend_constrains_project_set"; |
|
401 |
|
402 Goal "extend h F : stable A ==> F : stable (project_set h A)"; |
|
403 by (asm_full_simp_tac |
|
404 (simpset() addsimps [stable_def, extend_constrains_project_set]) 1); |
|
405 qed "extend_stable_project_set"; |
401 |
406 |
402 |
407 |
403 (*** Diff, needed for localTo ***) |
408 (*** Diff, needed for localTo ***) |
404 |
409 |
405 Goal "Restrict (extend_set h C) (extend_act h act) = \ |
410 Goal "Restrict (extend_set h C) (extend_act h act) = \ |