src/Provers/classical.ML
changeset 59119 c90c02940964
parent 58963 26bf09b95dda
child 59164 ff40c53d1af9
equal deleted inserted replaced
59118:fe7f91f85789 59119:c90c02940964
   137 instance, make_elim of Pure transforms the HOL rule injD into
   137 instance, make_elim of Pure transforms the HOL rule injD into
   138 
   138 
   139     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
   139     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
   140 
   140 
   141 Such rules can cause fast_tac to fail and blast_tac to report "PROOF
   141 Such rules can cause fast_tac to fail and blast_tac to report "PROOF
   142 FAILED"; classical_rule will strenthen this to
   142 FAILED"; classical_rule will strengthen this to
   143 
   143 
   144     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
   144     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
   145 *)
   145 *)
   146 
   146 
   147 fun classical_rule rule =
   147 fun classical_rule rule =