src/HOL/Integ/cooper_proof.ML
changeset 14920 a7525235e20f
parent 14877 28084696907f
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Thu Jun 10 20:17:07 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Sat Jun 12 13:50:55 2004 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  generation for Cooper Algorithm
     1.5  *)
     1.6  
     1.7 +
     1.8  signature COOPER_PROOF =
     1.9  sig
    1.10    val qe_Not : thm
    1.11 @@ -957,3 +958,4 @@
    1.12    end;
    1.13  
    1.14  end;
    1.15 +