equal
deleted
inserted
replaced
532 by (subgoal_tac |
532 by (subgoal_tac |
533 "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1); |
533 "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1); |
534 by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]); |
534 by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]); |
535 (*using Int_greatest actually slows the next step!*) |
535 (*using Int_greatest actually slows the next step!*) |
536 by (Blast_tac 2); |
536 by (Blast_tac 2); |
537 by (force_tac (claset(), |
537 by (rtac ccontr 1); |
538 simpset() addsimps [split_extended_all]) 1); |
538 by (dtac subsetD 1); |
|
539 by (Blast_tac 1); |
|
540 by (force_tac (claset(), simpset() addsimps [split_extended_all]) 1); |
539 qed "stable_project_transient"; |
541 qed "stable_project_transient"; |
540 |
542 |
541 |
543 |
542 Goal "[| G : stable C; project h C G : (project_set h C Int A) unless B |] \ |
544 Goal "[| G : stable C; project h C G : (project_set h C Int A) unless B |] \ |
543 \ ==> G : (C Int extend_set h A) unless (extend_set h B)"; |
545 \ ==> G : (C Int extend_set h A) unless (extend_set h B)"; |