# HG changeset patch # User paulson # Date 818416045 -3600 # Node ID 7095d6b89734da19fc621ca67e62c27cb5cbb64b # Parent a1d2735f5adeef606ab07e577b1fdb5e19e6ea5f improved indentation diff -r a1d2735f5ade -r 7095d6b89734 src/HOL/Sexp.thy --- a/src/HOL/Sexp.thy Fri Dec 08 10:39:52 1995 +0100 +++ b/src/HOL/Sexp.thy Fri Dec 08 10:47:25 1995 +0100 @@ -21,15 +21,15 @@ inductive "sexp" intrs LeafI "Leaf(a): sexp" - NumbI "Numb(a): sexp" + NumbI "Numb(i): sexp" SconsI "[| M: sexp; N: sexp |] ==> M$N : sexp" defs sexp_case_def "sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x)) - | (? k. M=Numb(k) & z=d(k)) - | (? N1 N2. M = N1 $ N2 & z=e N1 N2)" + | (? k. M=Numb(k) & z=d(k)) + | (? N1 N2. M = N1 $ N2 & z=e N1 N2)" pred_sexp_def "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"