# 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)}"