diff -r 66512c9e6bd6 -r c820b3cc3df0 src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/Qsort.thy	Wed Jun 21 15:47:10 1995 +0200
@@ -13,15 +13,15 @@
 rules
 
 qsort_Nil  "qsort le [] = []"
-qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ \
-\                            (x# qsort le [y:xs . le x y])"
+qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ 
+                            (x# qsort le [y:xs . le x y])"
 
 (* computational induction.
    The dependence of p on x but not xs is intentional.
 *)
 qsort_ind
- "[| P([]); \
-\    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> \
-\            P(x#xs) |] \
-\ ==> P(xs)"
+ "[| P([]); 
+    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> 
+            P(x#xs) |] 
+ ==> P(xs)"
 end