ex/qsort.thy

   qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
 
 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.
 *)
 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