--- a/ex/Qsort.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Qsort.thy Wed Mar 02 12:26:55 1994 +0100
@@ -13,8 +13,8 @@
rules
qsort_Nil "qsort(le,[]) = []"
-qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
-\ Cons(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.
@@ -22,6 +22,6 @@
qsort_ind
"[| P([]); \
\ !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
-\ P(Cons(x,xs)) |] \
+\ P(x#xs) |] \
\ ==> P(xs)"
end