Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Presburger/cooper_dec.ML
changeset 15661 9ef583b08647
parent 15574 b1d1b5bfc464
child 15859 7bc8b9683224 
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -92,7 +92,7 @@
 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
-(*SOME terms often used for pattern matching*) 
+(*Some terms often used for pattern matching*) 
  
 val zero = mk_numeral 0; 
 val one = mk_numeral 1;
isabelle