TFL/thms.sml
changeset 3273 114704740c86
parent 3245 241838c01caf
child 3302 404fe31fd8d2
equal deleted inserted replaced
3272:c93f54759539 3273:114704740c86
    24    in val LET_CONG = result() RS eq_reflection
    24    in val LET_CONG = result() RS eq_reflection
    25    end;
    25    end;
    26 
    26 
    27    val COND_CONG = if_cong RS eq_reflection;
    27    val COND_CONG = if_cong RS eq_reflection;
    28 
    28 
    29    fun C f x y = f y x;
    29    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    30    fun prover thl = [fast_tac HOL_cs 1];
       
    31    val P = C (prove_goal HOL.thy) prover;
       
    32 
    30 
    33    val eqT       = P"(x = True) --> x"
    31    val eqT       = prove"(x = True) --> x"
    34    val rev_eq_mp = P"(x = y) --> y --> x"
    32    val rev_eq_mp = prove"(x = y) --> y --> x"
    35    val simp_thm  = P"(x-->y) --> (x = x') --> (x' --> y)"
    33    val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"
    36 
    34 
    37 end;
    35 end;