--- 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