equal
deleted
inserted
replaced
847 |
847 |
848 (*Prove base case (subgoal i) and simplify others. A typical base case |
848 (*Prove base case (subgoal i) and simplify others. A typical base case |
849 concerns Crypt K X \\<notin> Key`shrK`bad and cannot be proved by rewriting |
849 concerns Crypt K X \\<notin> Key`shrK`bad and cannot be proved by rewriting |
850 alone.*) |
850 alone.*) |
851 fun prove_simple_subgoals_tac i = |
851 fun prove_simple_subgoals_tac i = |
852 force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN |
852 force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN |
853 ALLGOALS Asm_simp_tac; |
853 ALLGOALS Asm_simp_tac; |
854 |
854 |
855 fun Fake_parts_insert_tac i = |
855 fun Fake_parts_insert_tac i = |
856 blast_tac (claset() addIs [parts_insertI] |
856 blast_tac (claset() addIs [parts_insertI] |
857 addDs [impOfSubs analz_subset_parts, |
857 addDs [impOfSubs analz_subset_parts, |