]> matita.cs.unibo.it Git - helm.git/commitdiff
added library option to auto
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 20 Mar 2008 12:56:05 +0000 (12:56 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 20 Mar 2008 12:56:05 +0000 (12:56 +0000)
helm/software/matita/tests/paramodulation.ma

index 074dcc96a5e7a6b2fd20161a4e88efeca06d8253..eb2cbe17563e1573583acf276f2b31d785f4dbf1 100644 (file)
@@ -28,5 +28,5 @@ qed.
 
 theorem para2:
   \forall n:nat. n + n = 2 * n.
-intros. autobatch paramodulation.
+intros. autobatch paramodulation library.
 qed.