src/HOL/Sexp.ML
changeset 1642 21db0cf9a1a4
parent 1475 7f5a4cd08209
child 1760 6f41a494f3b1
     1.1 --- a/src/HOL/Sexp.ML	Thu Apr 04 11:43:25 1996 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Thu Apr 04 11:45:01 1996 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4  
     1.5  (** Introduction rules for 'pred_sexp' **)
     1.6  
     1.7 -goalw Sexp.thy [pred_sexp_def] "pred_sexp <= Sigma sexp (%u.sexp)";
     1.8 +goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
     1.9  by (fast_tac sexp_cs 1);
    1.10  qed "pred_sexp_subset_Sigma";
    1.11