--- a/src/HOL/hologic.ML Fri Dec 06 15:16:30 2002 +0100
+++ b/src/HOL/hologic.ML Mon Dec 09 10:38:56 2002 +0100
@@ -159,7 +159,7 @@
fun mk_UNIV T = Const ("UNIV", mk_setT T);
-(* binary oprations and relations *)
+(* binary operations and relations *)
fun mk_binop c (t, u) =
let val T = fastype_of t in
@@ -280,7 +280,7 @@
val binT = Type ("Numeral.bin", []);
-val pls_const = Const ("Numeral.bin.Pls", binT)
+val pls_const = Const ("Numeral.bin.Pls", binT)
and min_const = Const ("Numeral.bin.Min", binT)
and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);