X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Fmetasenv_ordering.ma;h=25c66594bc0f644bc07dd4f1cc3bbe22fd0844d5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=98b3ff0fea8c174ba9a65b5fb1ac6750d9f0ed55;hpb=78044035b4419e569df0d7f6a7f96fa32d21a19d;p=helm.git

diff --git a/helm/matita/tests/metasenv_ordering.ma b/helm/matita/tests/metasenv_ordering.ma
index 98b3ff0fe..25c66594b 100644
--- a/helm/matita/tests/metasenv_ordering.ma
+++ b/helm/matita/tests/metasenv_ordering.ma
@@ -25,11 +25,11 @@ theorem th1 :
    \forall P:Prop.
    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
    1 = 1 \land 1 = 0 \land 2 = 2.
-   intros. split. split.
-   goal 13.
-   rewrite > H; [reflexivity | exact nat | exact 0=0 | exact Type].     
-   reflexivity.
-   reflexivity.
+   intros. split; split;
+   [ reflexivity
+   | rewrite > H;
+     [ reflexivity | exact nat | exact (0=0) | exact Type ]
+   ]
 qed.    
     
 theorem th2 : 
@@ -37,8 +37,9 @@ theorem th2 :
    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
    1 = 1 \land 1 = 0 \land 3 = 3.
    intros. split. split.
-   goal 13.
-   rewrite > H ?; [reflexivity | exact nat | exact 0=0 | exact Type].     
+   focus 13.
+     rewrite > (H ?); [reflexivity | exact nat | exact (0=0) | exact Type].     
+   unfocus.
    reflexivity.
    reflexivity.
 qed.       
@@ -48,8 +49,9 @@ theorem th3 :
    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
    1 = 1 \land 1 = 0 \land 4 = 4.
    intros. split. split.
-   goal 13.
-   rewrite > H ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].     
+   focus 13.
+     rewrite > (H ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+   unfocus.     
    reflexivity.
    reflexivity.
 qed. 
@@ -59,8 +61,9 @@ theorem th4 :
    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
    1 = 1 \land 1 = 0 \land 5 = 5.
    intros. split. split.
-   goal 13.
-   rewrite > H ? ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].     
+   focus 13.
+     rewrite > (H ? ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+   unfocus.     
    reflexivity.
    reflexivity.
 qed. 
@@ -72,8 +75,9 @@ theorem th5 :
    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
    1 = 1 \land 1 = 0 \land 6 = 6.
    intros. split. split.
-   goal 13.
-   apply H; [exact nat | exact 0=0 | exact Type].     
+   focus 13.
+     apply H; [exact nat | exact (0=0) | exact Type].
+   unfocus.     
    reflexivity.
    reflexivity.
 qed. 
@@ -83,8 +87,9 @@ theorem th6 :
    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
    1 = 1 \land 1 = 0 \land 7 = 7.
    intros. split. split.
-   goal 13.
-   apply H ?; [exact nat | exact 0=0 | exact Type].     
+   focus 13.
+     apply (H ?); [exact nat | exact (0=0) | exact Type].
+   unfocus.     
    reflexivity.
    reflexivity.
 qed.
@@ -94,8 +99,9 @@ theorem th7 :
    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
    1 = 1 \land 1 = 0 \land 8 = 8.
    intros. split. split.
-   goal 13.
-   apply H ? ?; [exact nat | exact 0=0 | exact Type].     
+   focus 13.
+     apply (H ? ?); [exact nat | exact (0=0) | exact Type].
+   unfocus.     
    reflexivity.
    reflexivity.
 qed.     
@@ -105,8 +111,9 @@ theorem th8 :
    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
    1 = 1 \land 1 = 0 \land 9 = 9.
    intros. split. split.
-   goal 13.
-   apply H ? ? ?; [exact nat | exact 0=0 | exact Type].     
+   focus 13.
+     apply (H ? ? ?); [exact nat | exact (0=0) | exact Type].
+   unfocus.     
    reflexivity.
    reflexivity.
 qed.
@@ -115,28 +122,18 @@ qed.
 
 theorem th9:
   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
-  intros [P; Q; R; S; r; s; H].
-  elim H ? ?; [split; assumption | exact r | exact s].
+  intros (P Q R S r s H).
+  elim (H ? ?); [split; assumption | exact r | exact s].
   qed.
  
 theorem th10:
   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
-  intros [P; Q; R; S; r; s; H].
-  elim H ?; [split; assumption | exact r | exact s].
+  intros (P Q R S r s H).
+  elim (H ?); [split; assumption | exact r | exact s].
   qed.
   
 theorem th11:
   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
-  intros [P; Q; R; S; r; s; H].
+  intros (P Q R S r s H).
   elim H; [split; assumption | exact r | exact s].
   qed.
-  
-
-  
-   
-  
-  
-         
-      
-      
-      
\ No newline at end of file