src/HOL/Sexp.thy
changeset 1395 7095d6b89734
parent 1370 7361ac9b024d
child 1475 7f5a4cd08209
     1.1 --- a/src/HOL/Sexp.thy	Fri Dec 08 10:39:52 1995 +0100
     1.2 +++ b/src/HOL/Sexp.thy	Fri Dec 08 10:47:25 1995 +0100
     1.3 @@ -21,15 +21,15 @@
     1.4  inductive "sexp"
     1.5    intrs
     1.6      LeafI  "Leaf(a): sexp"
     1.7 -    NumbI  "Numb(a): sexp"
     1.8 +    NumbI  "Numb(i): sexp"
     1.9      SconsI "[| M: sexp;  N: sexp |] ==> M$N : sexp"
    1.10  
    1.11  defs
    1.12  
    1.13    sexp_case_def	
    1.14     "sexp_case c d e M == @ z. (? x.   M=Leaf(x) & z=c(x))  
    1.15 -                           | (? k.   M=Numb(k) & z=d(k))  
    1.16 -                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
    1.17 +                            | (? k.   M=Numb(k) & z=d(k))  
    1.18 +                            | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
    1.19  
    1.20    pred_sexp_def
    1.21       "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"