Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/classical.ML
changeset 26938 64e850c3da9e
parent 26928 ca87aff1ad2d
child 29267 8615b4f54047 
--- a/src/Provers/classical.ML	Sat May 17 23:53:19 2008 +0200
+++ b/src/Provers/classical.ML	Sat May 17 23:53:20 2008 +0200
@@ -170,7 +170,7 @@
 
     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
 
-Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF
+Such rules can cause fast_tac to fail and blast_tac to report "PROOF
 FAILED"; classical_rule will strenthen this to
 
     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
isabelle