src/HOL/HOL.ML
changeset 4025 77e426be5624
parent 3842 b55686a7b22c
child 4087 42229596565c
equal deleted inserted replaced
4024:3c056eab237c 4025:77e426be5624
    75 section "True";
    75 section "True";
    76 
    76 
    77 qed_goalw "TrueI" HOL.thy [True_def] "True"
    77 qed_goalw "TrueI" HOL.thy [True_def] "True"
    78   (fn _ => [rtac refl 1]);
    78   (fn _ => [rtac refl 1]);
    79 
    79 
    80 qed_goal "eqTrueI " HOL.thy "P ==> P=True" 
    80 qed_goal "eqTrueI" HOL.thy "P ==> P=True" 
    81  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
    81  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
    82 
    82 
    83 qed_goal "eqTrueE" HOL.thy "P=True ==> P" 
    83 qed_goal "eqTrueE" HOL.thy "P=True ==> P" 
    84  (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
    84  (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
    85 
    85