src/HOL/Sexp.ML
changeset 1465 5d7a7e439cec
parent 1264 3eb91524b938
child 1475 7f5a4cd08209
     1.1 --- a/src/HOL/Sexp.ML	Tue Jan 30 15:19:20 1996 +0100
     1.2 +++ b/src/HOL/Sexp.ML	Tue Jan 30 15:24:36 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOL/Sexp
     1.5 +(*  Title:      HOL/Sexp
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1994  University of Cambridge
    1.10  
    1.11  S-expressions, general binary trees for defining recursive data structures
    1.12 @@ -12,22 +12,22 @@
    1.13  
    1.14  val sexp_free_cs = 
    1.15      set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject] 
    1.16 -	   addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
    1.17 -		   Numb_neq_Scons, Numb_neq_Leaf,
    1.18 -		   Scons_neq_Leaf, Scons_neq_Numb];
    1.19 +           addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
    1.20 +                   Numb_neq_Scons, Numb_neq_Leaf,
    1.21 +                   Scons_neq_Leaf, Scons_neq_Numb];
    1.22  
    1.23  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    1.24 -by (resolve_tac [select_equality] 1);
    1.25 +by (rtac select_equality 1);
    1.26  by (ALLGOALS (fast_tac sexp_free_cs));
    1.27  qed "sexp_case_Leaf";
    1.28  
    1.29  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    1.30 -by (resolve_tac [select_equality] 1);
    1.31 +by (rtac select_equality 1);
    1.32  by (ALLGOALS (fast_tac sexp_free_cs));
    1.33  qed "sexp_case_Numb";
    1.34  
    1.35  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
    1.36 -by (resolve_tac [select_equality] 1);
    1.37 +by (rtac select_equality 1);
    1.38  by (ALLGOALS (fast_tac sexp_free_cs));
    1.39  qed "sexp_case_Scons";
    1.40  
    1.41 @@ -88,7 +88,7 @@
    1.42  
    1.43  (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
    1.44  Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
    1.45 -	                pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
    1.46 +                        pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
    1.47  
    1.48  val major::prems = goalw Sexp.thy [pred_sexp_def]
    1.49      "[| p : pred_sexp;  \