src/HOL/simpdata.ML
changeset 12975 d796a2fd6c69
parent 12725 7ede865e1fe5
child 13462 56610e2ba220
     1.1 --- a/src/HOL/simpdata.ML	Thu Feb 28 17:21:48 2002 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Thu Feb 28 17:46:46 2002 +0100
     1.3 @@ -277,6 +277,11 @@
     1.4  by (etac arg_cong 1);
     1.5  qed "let_weak_cong";
     1.6  
     1.7 +(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
     1.8 +Goal "u = u' ==> (t==u) == (t==u')";
     1.9 +by (asm_simp_tac HOL_ss 1);
    1.10 +qed "eq_cong2";
    1.11 +
    1.12  Goal "f(if c then x else y) = (if c then f x else f y)";
    1.13  by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
    1.14  qed "if_distrib";