src/HOL/Sexp.ML
changeset 5143 b94cd208f073
parent 5069 3ea049f7979d
child 5191 8ceaa19f7717
     1.1 --- a/src/HOL/Sexp.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4  by (rtac sexp_case_Numb 1);
     1.5  qed "sexp_rec_Numb";
     1.6  
     1.7 -Goal "!!M. [| M: sexp;  N: sexp |] ==> \
     1.8 +Goal "[| M: sexp;  N: sexp |] ==> \
     1.9  \    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
    1.10  by (rtac (sexp_rec_unfold RS trans) 1);
    1.11  by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);