src/HOL/Sexp.thy
changeset 972 e61b058d58d2
parent 923 ff1574a81019
child 1151 c820b3cc3df0
     1.1 --- a/src/HOL/Sexp.thy	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/Sexp.thy	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  \                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
     1.5  
     1.6    pred_sexp_def
     1.7 -     "pred_sexp == UN M: sexp. UN N: sexp. {<M, M$N>, <N, M$N>}"
     1.8 +     "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
     1.9  
    1.10    sexp_rec_def
    1.11     "sexp_rec M c d e == wfrec pred_sexp M  \