src/HOL/Quot/NPAIR.ML
changeset 4477 b3e5857d8d99
parent 3457 a8ab7c64817c
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Quot/NPAIR.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Quot/NPAIR.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -7,13 +7,13 @@
     1.4  open NPAIR;
     1.5  
     1.6  goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed "rep_abs_NP";
    1.10  
    1.11  Addsimps [rep_abs_NP];
    1.12  
    1.13  val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
    1.14  by (cut_facts_tac prems 1);
    1.15 -by (Auto_tac());
    1.16 +by Auto_tac;
    1.17  qed "per_sym_NP";
    1.18