src/HOL/Sexp.ML
changeset 972 e61b058d58d2
parent 923 ff1574a81019
child 1264 3eb91524b938
     1.1 --- a/src/HOL/Sexp.ML	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/Sexp.ML	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -63,19 +63,19 @@
     1.4  by (fast_tac sexp_cs 1);
     1.5  qed "pred_sexp_subset_Sigma";
     1.6  
     1.7 -(* <a,b> : pred_sexp^+ ==> a : sexp *)
     1.8 +(* (a,b) : pred_sexp^+ ==> a : sexp *)
     1.9  val trancl_pred_sexpD1 = 
    1.10      pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
    1.11  and trancl_pred_sexpD2 = 
    1.12      pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
    1.13  
    1.14  val prems = goalw Sexp.thy [pred_sexp_def]
    1.15 -    "[| M: sexp;  N: sexp |] ==> <M, M$N> : pred_sexp";
    1.16 +    "[| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
    1.17  by (fast_tac (set_cs addIs prems) 1);
    1.18  qed "pred_sexpI1";
    1.19  
    1.20  val prems = goalw Sexp.thy [pred_sexp_def]
    1.21 -    "[| M: sexp;  N: sexp |] ==> <N, M$N> : pred_sexp";
    1.22 +    "[| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
    1.23  by (fast_tac (set_cs addIs prems) 1);
    1.24  qed "pred_sexpI2";
    1.25  
    1.26 @@ -86,7 +86,7 @@
    1.27  val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
    1.28  and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
    1.29  
    1.30 -(*Proves goals of the form <M,N>:pred_sexp^+ provided M,N:sexp*)
    1.31 +(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
    1.32  val pred_sexp_simps =
    1.33              sexp.intrs @
    1.34  	    [pred_sexp_t1, pred_sexp_t2,
    1.35 @@ -95,8 +95,8 @@
    1.36  
    1.37  val major::prems = goalw Sexp.thy [pred_sexp_def]
    1.38      "[| p : pred_sexp;  \
    1.39 -\       !!M N. [| p = <M, M$N>;  M: sexp;  N: sexp |] ==> R; \
    1.40 -\       !!M N. [| p = <N, M$N>;  M: sexp;  N: sexp |] ==> R  \
    1.41 +\       !!M N. [| p = (M, M$N);  M: sexp;  N: sexp |] ==> R; \
    1.42 +\       !!M N. [| p = (N, M$N);  M: sexp;  N: sexp |] ==> R  \
    1.43  \    |] ==> R";
    1.44  by (cut_facts_tac [major] 1);
    1.45  by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));