
diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Induct/SList.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -10,8 +10,8 @@
 
 Definition of type 'a list (strict lists) by a least fixed point
 
-We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
-and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
+We use          list(A) == lfp(%Z. {NUMB(0)} <+> A \<times> Z)
+and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) \<times> Z)
 
 so that list can serve as a "functor" for defining other recursive types.
 




