...

[helm.git] / helm / software / matita / library / demo / formal_topology.ma

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 56a8c4120b802e3b65dc73f14417820c22d58855..8e957e8b64975bf8942be23ee6c3900097493e91 100644 (file)
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -122,7 +122,7 @@ theorem covers_elim2:
     simplify in H4 ⊢ %;
     apply H1;
      [ apply (C ? a1 j);
-     | autobatch;
+     | autobatch; 
      | assumption;
      | assumption]]
 qed.