src/HOL/Integ/cooper_proof.ML
changeset 15661 9ef583b08647
parent 15531 08c8dad8e399
child 16389 48832eba5b1e
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Thu Apr 07 09:24:35 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Thu Apr 07 09:25:33 2005 +0200
     1.3 @@ -380,7 +380,7 @@
     1.4  (*==================================================*)
     1.5  fun rho_for_modd_minf x dlcm sg fm1 =
     1.6  let
     1.7 -    (*SOME certified Terms*)
     1.8 +    (*Some certified Terms*)
     1.9      
    1.10     val ctrue = cterm_of sg HOLogic.true_const
    1.11     val cfalse = cterm_of sg HOLogic.false_const
    1.12 @@ -476,7 +476,7 @@
    1.13  (* -------------------------------------------------------------*)
    1.14  fun rho_for_modd_pinf x dlcm sg fm1 = 
    1.15  let
    1.16 -    (*SOME certified Terms*)
    1.17 +    (*Some certified Terms*)
    1.18      
    1.19    val ctrue = cterm_of sg HOLogic.true_const
    1.20    val cfalse = cterm_of sg HOLogic.false_const