src/HOL/Sexp.ML
changeset 5278 a903b66822e2
parent 5191 8ceaa19f7717
child 5440 f099dffd0f18
     1.1 --- a/src/HOL/Sexp.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -98,8 +98,7 @@
     1.4  
     1.5  (*** sexp_rec -- by wf recursion on pred_sexp ***)
     1.6  
     1.7 -Goal
     1.8 -   "(%M. sexp_rec M c d e) = wfrec pred_sexp \
     1.9 +Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
    1.10                         \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
    1.11  by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
    1.12