# HG changeset patch # User oheimb # Date 946904830 -3600 # Node ID f0d4165bc534a152f2906aeafe3eceb3ef87d64c # Parent 381716a86fcb9f81fe24a521631c123cfcfc2c49 removed inj_eq from the default simpset again diff -r 381716a86fcb -r f0d4165bc534 src/HOL/MicroJava/J/JBasis.ML --- 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} \\ {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])];