Proved and added rewrite rule (@x. x=y) = y to simpset.
authornipkow
Wed Sep 09 17:34:58 1998 +0200 (1998-09-09)
changeset 5447df03d330aeab
parent 5446 506259e4e546
child 5448 40a09282ba14
Proved and added rewrite rule (@x. x=y) = y to simpset.
Strange that only the symetric version was present!
src/HOL/HOL.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.ML	Wed Sep 09 17:25:49 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Wed Sep 09 17:34:58 1998 +0200
     1.3 @@ -297,7 +297,12 @@
     1.4          etac exE 1,
     1.5          etac selectI 1]);
     1.6  
     1.7 -qed_goal "Eps_eq" HOL.thy "(Eps (op = x)) = x" (K [
     1.8 +qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
     1.9 +	rtac select_equality 1,
    1.10 +	rtac refl 1,
    1.11 +	atac 1]);
    1.12 +
    1.13 +qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
    1.14  	rtac select_equality 1,
    1.15  	rtac refl 1,
    1.16  	etac sym 1]);
     2.1 --- a/src/HOL/simpdata.ML	Wed Sep 09 17:25:49 1998 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Wed Sep 09 17:34:58 1998 +0200
     2.3 @@ -420,7 +420,7 @@
     2.4         if_True, if_False, if_cancel, if_eq_cancel,
     2.5         imp_disjL, conj_assoc, disj_assoc,
     2.6         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
     2.7 -       disj_not1, not_all, not_ex, cases_simp, Eps_eq]
     2.8 +       disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq]
     2.9       @ ex_simps @ all_simps @ simp_thms)
    2.10       addsimprocs [defALL_regroup,defEX_regroup]
    2.11       addcongs [imp_cong]