equal
deleted
inserted
replaced
860 |
860 |
861 (*Prove base case (subgoal i) and simplify others. A typical base case |
861 (*Prove base case (subgoal i) and simplify others. A typical base case |
862 concerns Crypt K X ~: Key``shrK``bad and cannot be proved by rewriting |
862 concerns Crypt K X ~: Key``shrK``bad and cannot be proved by rewriting |
863 alone.*) |
863 alone.*) |
864 fun prove_simple_subgoals_tac i = |
864 fun prove_simple_subgoals_tac i = |
865 fast_tac (claset() addss (simpset())) i THEN |
865 Force_tac i THEN ALLGOALS Asm_simp_tac; |
866 ALLGOALS Asm_simp_tac; |
|
867 |
866 |
868 fun Fake_parts_insert_tac i = |
867 fun Fake_parts_insert_tac i = |
869 blast_tac (claset() addIs [parts_insertI] |
868 blast_tac (claset() addIs [parts_insertI] |
870 addDs [impOfSubs analz_subset_parts, |
869 addDs [impOfSubs analz_subset_parts, |
871 impOfSubs Fake_parts_insert]) i; |
870 impOfSubs Fake_parts_insert]) i; |