Had to remove {x.x=a} = a from !simpset in one proof.
authornipkow
Fri Aug 01 09:41:38 1997 +0200 (1997-08-01)
changeset 35835a47b869d16a
parent 3582 b87c86b6c291
child 3584 8f9ee0f79d9a
Had to remove {x.x=a} = a from !simpset in one proof.
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Aug 01 09:39:28 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Aug 01 09:41:38 1997 +0200
     1.3 @@ -524,7 +524,7 @@
     1.4  
     1.5  
     1.6  goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
     1.7 -by (asm_simp_tac (!simpset addsimps [insert_def] 
     1.8 +by (asm_simp_tac (!simpset addsimps [insert_def] delsimps [singleton_conv]
     1.9                             setloop (rtac analz_cong)) 1);
    1.10  qed "analz_insert_cong";
    1.11