src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 56245 84fc7dfa3cd4
parent 56220 4c43a2881b25
child 56252 b72e0a9d62b9
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -1670,7 +1670,7 @@
     1.4     (* @{const_name HOL.not_equal}, *)
     1.5     @{const_name HOL.False},
     1.6     @{const_name HOL.True},
     1.7 -   @{const_name "==>"}]
     1.8 +   @{const_name Pure.imp}]
     1.9  
    1.10  fun strip_qtfrs_tac ctxt =
    1.11    REPEAT_DETERM (HEADGOAL (rtac @{thm allI}))