src/HOL/Sexp.thy
changeset 1151 c820b3cc3df0
parent 972 e61b058d58d2
child 1370 7361ac9b024d
     1.1 --- a/src/HOL/Sexp.thy	Wed Jun 21 15:14:58 1995 +0200
     1.2 +++ b/src/HOL/Sexp.thy	Wed Jun 21 15:47:10 1995 +0200
     1.3 @@ -10,11 +10,11 @@
     1.4  consts
     1.5    sexp      :: "'a item set"
     1.6  
     1.7 -  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, \
     1.8 -\                'a item] => 'b"
     1.9 +  sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
    1.10 +                'a item] => 'b"
    1.11  
    1.12 -  sexp_rec  :: "['a item, 'a=>'b, nat=>'b, 	\
    1.13 -\                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
    1.14 +  sexp_rec  :: "['a item, 'a=>'b, nat=>'b, 	
    1.15 +                ['a item, 'a item, 'b, 'b]=>'b] => 'b"
    1.16    
    1.17    pred_sexp :: "('a item * 'a item)set"
    1.18  
    1.19 @@ -27,14 +27,14 @@
    1.20  defs
    1.21  
    1.22    sexp_case_def	
    1.23 -   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  \
    1.24 -\                           | (? k.   M=Numb(k) & z=d(k))  \
    1.25 -\                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
    1.26 +   "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
    1.27 +                           | (? k.   M=Numb(k) & z=d(k))  
    1.28 +                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
    1.29  
    1.30    pred_sexp_def
    1.31       "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
    1.32  
    1.33    sexp_rec_def
    1.34 -   "sexp_rec M c d e == wfrec pred_sexp M  \
    1.35 -\             (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
    1.36 +   "sexp_rec M c d e == wfrec pred_sexp M  
    1.37 +             (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
    1.38  end