src/HOL/Real/PNat.ML

 (***) (***) (***) (***) (***) (***) (***) (***) (***)
 
   (*** pnat_less ***)
 
 Goalw [pnat_less_def] 
-      "!!x. [| x < (y::pnat); y < z |] ==> x < z";
+      "[| x < (y::pnat); y < z |] ==> x < z";
 by ((etac less_trans 1) THEN assume_tac 1);
 qed "pnat_less_trans";
 
 Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x";
 by (etac less_not_sym 1);

 qed "pnat_less_not_refl";
 
 bind_thm ("pnat_less_irrefl",pnat_less_not_refl RS notE);
 
 Goalw [pnat_less_def] 
-     "!!x. x < (y::pnat) ==> x ~= y";
+     "x < (y::pnat) ==> x ~= y";
 by Auto_tac;
 qed "pnat_less_not_refl2";
 
 Goal "~ Rep_pnat y < 0";
 by Auto_tac;

 
 (*** Rep_pnat < 1 ==> P ***)
 bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
 
 Goalw [pnat_less_def] 
-     "!!x. x < (y::pnat) ==> Rep_pnat y ~= 1";
+     "x < (y::pnat) ==> Rep_pnat y ~= 1";
 by (auto_tac (claset(),simpset() 
     addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
 qed "Rep_pnat_gt_implies_not0";
 
 Goalw [pnat_less_def] 

 by (auto_tac (claset() addIs [add_less_mono],
        simpset() addsimps [sum_Rep_pnat_sum RS sym]));
 qed "pnat_add_less_mono";
 
 Goalw [pnat_less_def]
-     "!!f. [| !!i j::pnat. i<j ==> f(i) < f(j);       \
+"!!f. [| !!i j::pnat. i<j ==> f(i) < f(j);       \
 \        i <= j                                 \
 \     |] ==> f(i) <= (f(j)::pnat)";
 by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD],
              simpset() addsimps [pnat_le_iff_Rep_pnat_le,
                                      le_eq_less_or_eq]));