author | oheimb |
Mon, 03 Jan 2000 14:07:10 +0100 | |
changeset 8083 | f0d4165bc534 |
parent 8082 | 381716a86fcb |
child 8084 | c3790c6b4470 |
--- a/src/HOL/MicroJava/J/JBasis.ML Mon Jan 03 14:07:08 2000 +0100 +++ b/src/HOL/MicroJava/J/JBasis.ML Mon Jan 03 14:07:10 2000 +0100 @@ -67,10 +67,6 @@ rotate_tac ~1,asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])]; -Goal "{y. x = Some y} \\<subseteq> {the x}"; -by Auto_tac; -qed "some_subset_the"; - fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1, asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];