changed syntax of tuples from <..., ...> to (..., ...)
authorclasohm
Fri Mar 24 12:30:35 1995 +0100 (1995-03-24)
changeset 972e61b058d58d2
parent 971 f4815812665b
child 973 f57fb576520f
changed syntax of tuples from <..., ...> to (..., ...)
src/HOL/Arith.ML
src/HOL/Arith.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Equiv.ML
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Hoare.thy
src/HOL/IOA/meta_theory/Asig.thy
src/HOL/IOA/meta_theory/IOA.ML
src/HOL/IOA/meta_theory/IOA.thy
src/HOL/IOA/meta_theory/Solve.ML
src/HOL/IOA/meta_theory/Solve.thy
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Equiv.thy
src/HOL/Integ/Integ.ML
src/HOL/Integ/Integ.thy
src/HOL/Integ/Relation.ML
src/HOL/Integ/Relation.thy
src/HOL/Nat.ML
src/HOL/Nat.thy
src/HOL/Prod.ML
src/HOL/Prod.thy
src/HOL/Sexp.ML
src/HOL/Sexp.thy
src/HOL/Subst/AList.ML
src/HOL/Subst/Subst.ML
src/HOL/Subst/Subst.thy
src/HOL/Subst/Unifier.ML
src/HOL/Trancl.ML
src/HOL/Trancl.thy
src/HOL/Univ.ML
src/HOL/Univ.thy
src/HOL/WF.ML
src/HOL/WF.thy
src/HOL/ex/Acc.ML
src/HOL/ex/Acc.thy
src/HOL/ex/LList.ML
src/HOL/ex/LList.thy
src/HOL/ex/LexProd.ML
src/HOL/ex/LexProd.thy
src/HOL/ex/MT.ML
src/HOL/ex/MT.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/SList.ML
src/HOL/ex/Term.ML
src/HOL/ex/rel.ML
     1.1 --- a/src/HOL/Arith.ML	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/Arith.ML	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -175,7 +175,7 @@
     1.4  
     1.5  val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans);
     1.6  
     1.7 -goalw Nat.thy [less_def] "<m,n> : pred_nat^+ = (m<n)";
     1.8 +goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)";
     1.9  by (rtac refl 1);
    1.10  qed "less_eq";
    1.11  
     2.1 --- a/src/HOL/Arith.thy	Thu Mar 23 15:39:13 1995 +0100
     2.2 +++ b/src/HOL/Arith.thy	Fri Mar 24 12:30:35 1995 +0100
     2.3 @@ -26,6 +26,6 @@
     2.4  
     2.5  (*"Difference" is subtraction of natural numbers.
     2.6    There are no negative numbers; we have
     2.7 -     m - n = 0  iff  m<=n   and     m - n = Suc(k) iff m>n.
     2.8 +     m - n = 0  iff  m<=n   and     m - n = Suc(k) iff m)n.
     2.9    Also, nat_rec(m, 0, %z w.z) is pred(m).   *)
    2.10  
     3.1 --- a/src/HOL/IMP/Com.thy	Thu Mar 23 15:39:13 1995 +0100
     3.2 +++ b/src/HOL/IMP/Com.thy	Fri Mar 24 12:30:35 1995 +0100
     3.3 @@ -26,9 +26,9 @@
     3.4  
     3.5  (** Evaluation of arithmetic expressions **)
     3.6  consts  evala    :: "(aexp*state*nat)set"
     3.7 -       "@evala"  :: "[aexp,state,nat] => bool"	("<_,_>/ -a-> _"  [0,0,50] 50)
     3.8 +       "@evala"  :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _"  [0,0,50] 50)
     3.9  translations
    3.10 -    "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
    3.11 +    "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
    3.12  inductive "evala"
    3.13    intrs 
    3.14      N   "<N(n),s> -a-> n"
    3.15 @@ -51,10 +51,10 @@
    3.16  
    3.17  (** Evaluation of boolean expressions **)
    3.18  consts evalb	:: "(bexp*state*bool)set"	
    3.19 -       "@evalb" :: "[bexp,state,bool] => bool"	("<_,_>/ -b-> _"  [0,0,50] 50)
    3.20 +       "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _"  [0,0,50] 50)
    3.21  
    3.22  translations
    3.23 -    "<be,sig> -b-> b" == "<be,sig,b> : evalb"
    3.24 +    "<be,sig> -b-> b" == "(be,sig,b) : evalb"
    3.25  
    3.26  inductive "evalb"
    3.27   intrs (*avoid clash with ML constructors true, false*)
    3.28 @@ -79,11 +79,11 @@
    3.29  
    3.30  (** Execution of commands **)
    3.31  consts  evalc    :: "(com*state*state)set"
    3.32 -        "@evalc" :: "[com,state,state] => bool"  ("<_,_>/ -c-> _" [0,0,50] 50)
    3.33 -	"assign" :: "[state,nat,loc] => state"   ("_[_'/_]"       [95,0,0] 95)
    3.34 +        "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
    3.35 +	"assign" :: "[state,nat,loc] => state"  ("_[_'/_]"       [95,0,0] 95)
    3.36  
    3.37  translations
    3.38 -       "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
    3.39 +       "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
    3.40  
    3.41  rules 
    3.42  	assign_def	"s[m/x] == (%y. if y=x then m else s y)"
     4.1 --- a/src/HOL/IMP/Equiv.ML	Thu Mar 23 15:39:13 1995 +0100
     4.2 +++ b/src/HOL/IMP/Equiv.ML	Fri Mar 24 12:30:35 1995 +0100
     4.3 @@ -25,7 +25,7 @@
     4.4  val BfstD = read_instantiate_sg (sign_of Equiv.thy)
     4.5                [("P","%x.B ?b x")] (fst_conv RS subst);
     4.6  
     4.7 -goal Equiv.thy "!!c. <c,s> -c-> t ==> <s,t> : C(c)";
     4.8 +goal Equiv.thy "!!c. <c,s> -c-> t ==> (s,t) : C(c)";
     4.9  
    4.10  (* start with rule induction *)
    4.11  be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
     5.1 --- a/src/HOL/IMP/Hoare.ML	Thu Mar 23 15:39:13 1995 +0100
     5.2 +++ b/src/HOL/IMP/Hoare.ML	Fri Mar 24 12:30:35 1995 +0100
     5.3 @@ -39,8 +39,8 @@
     5.4  qed"hoare_if";
     5.5  
     5.6  val major::prems = goal Hoare.thy
     5.7 -  "[| <a,b> :lfp f; mono f; \
     5.8 -\     !!a b. <a,b> : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
     5.9 +  "[| (a,b) :lfp f; mono f; \
    5.10 +\     !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
    5.11  by(res_inst_tac [("c1","P")] (split RS subst) 1);
    5.12  br (major RS induct) 1;
    5.13  brs prems 1;
     6.1 --- a/src/HOL/IMP/Hoare.thy	Thu Mar 23 15:39:13 1995 +0100
     6.2 +++ b/src/HOL/IMP/Hoare.thy	Fri Mar 24 12:30:35 1995 +0100
     6.3 @@ -12,7 +12,7 @@
     6.4  (* syntax "@spec" :: "[bool,com,bool] => bool" *)
     6.5            ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
     6.6  defs
     6.7 -  spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"
     6.8 +  spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
     6.9  end
    6.10  (* Pretty-printing of assertions.
    6.11     Not very helpful as long as programs are not pretty-printed.
     7.1 --- a/src/HOL/IOA/meta_theory/Asig.thy	Thu Mar 23 15:39:13 1995 +0100
     7.2 +++ b/src/HOL/IOA/meta_theory/Asig.thy	Fri Mar 24 12:30:35 1995 +0100
     7.3 @@ -39,7 +39,7 @@
     7.4  
     7.5  
     7.6  mk_ext_asig_def
     7.7 -  "mk_ext_asig(triple) == <inputs(triple), outputs(triple), {}>"
     7.8 +  "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
     7.9  
    7.10  
    7.11  end 
     8.1 --- a/src/HOL/IOA/meta_theory/IOA.ML	Thu Mar 23 15:39:13 1995 +0100
     8.2 +++ b/src/HOL/IOA/meta_theory/IOA.ML	Fri Mar 24 12:30:35 1995 +0100
     8.3 @@ -13,12 +13,12 @@
     8.4  val exec_rws = [executions_def,is_execution_fragment_def];
     8.5  
     8.6  goal IOA.thy
     8.7 -"asig_of(<x,y,z>) = x & starts_of(<x,y,z>) = y & trans_of(<x,y,z>) = z";
     8.8 +"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z";
     8.9    by (simp_tac (SS addsimps ioa_projections) 1);
    8.10    qed "ioa_triple_proj";
    8.11  
    8.12  goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def]
    8.13 -  "!!A. [| IOA(A); <s1,a,s2>:trans_of(A) |] ==> a:actions(asig_of(A))";
    8.14 +  "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))";
    8.15    by (REPEAT(etac conjE 1));
    8.16    by (EVERY1[etac allE, etac impE, atac]);
    8.17    by (asm_full_simp_tac SS 1);
    8.18 @@ -45,18 +45,18 @@
    8.19  qed "mk_behaviour_thm";
    8.20  
    8.21  goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
    8.22 -  by (res_inst_tac [("x","<%i.None,%i.s>")] bexI 1);
    8.23 +  by (res_inst_tac [("x","(%i.None,%i.s)")] bexI 1);
    8.24    by (simp_tac SS 1);
    8.25    by (asm_simp_tac (SS addsimps exec_rws) 1);
    8.26  qed "reachable_0";
    8.27  
    8.28  goalw IOA.thy (reachable_def::exec_rws)
    8.29 -"!!A. [| reachable A s; <s,a,t> : trans_of(A) |] ==> reachable A t";
    8.30 +"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
    8.31    by(asm_full_simp_tac SS 1);
    8.32    by(safe_tac set_cs);
    8.33 -  by(res_inst_tac [("x","<%i.if i<n then fst ex i                    \
    8.34 +  by(res_inst_tac [("x","(%i.if i<n then fst ex i                    \
    8.35  \                            else (if i=n then Some a else None),    \
    8.36 -\                         %i.if i<Suc n then snd ex i else t>")] bexI 1);
    8.37 +\                         %i.if i<Suc n then snd ex i else t)")] bexI 1);
    8.38    by(res_inst_tac [("x","Suc(n)")] exI 1);
    8.39    by(simp_tac SS 1);
    8.40    by(asm_simp_tac (SS delsimps [less_Suc_eq]) 1);
    8.41 @@ -73,7 +73,7 @@
    8.42  
    8.43  val [p1,p2] = goalw IOA.thy [invariant_def]
    8.44    "[| !!s. s:starts_of(A) ==> P(s);                                          \
    8.45 -\     !!s t a. [|reachable A s; P(s)|] ==> <s,a,t>: trans_of(A) --> P(t) |] \
    8.46 +\     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
    8.47  \  ==> invariant A P";
    8.48    by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
    8.49    by (safe_tac set_cs);
    8.50 @@ -91,7 +91,7 @@
    8.51  
    8.52  val [p1,p2] = goal IOA.thy
    8.53   "[| !!s. s : starts_of(A) ==> P(s); \
    8.54 -\   !!s t a. reachable A s ==> P(s) --> <s,a,t>:trans_of(A) --> P(t) \
    8.55 +\   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
    8.56  \ |] ==> invariant A P";
    8.57    by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
    8.58  qed "invariantI1";
    8.59 @@ -121,18 +121,18 @@
    8.60  
    8.61  
    8.62  goal IOA.thy 
    8.63 -"<s,a,t> : trans_of(A || B || C || D) =                                      \
    8.64 +"(s,a,t) : trans_of(A || B || C || D) =                                      \
    8.65  \ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
    8.66  \   a:actions(asig_of(D))) &                                                 \
    8.67 -\  (if a:actions(asig_of(A)) then <fst(s),a,fst(t)>:trans_of(A)              \
    8.68 +\  (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)              \
    8.69  \   else fst t=fst s) &                                                      \
    8.70 -\  (if a:actions(asig_of(B)) then <fst(snd(s)),a,fst(snd(t))>:trans_of(B)    \
    8.71 +\  (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)    \
    8.72  \   else fst(snd(t))=fst(snd(s))) &                                          \
    8.73  \  (if a:actions(asig_of(C)) then                                            \
    8.74 -\     <fst(snd(snd(s))),a,fst(snd(snd(t)))>:trans_of(C)                      \
    8.75 +\     (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)                      \
    8.76  \   else fst(snd(snd(t)))=fst(snd(snd(s)))) &                                \
    8.77  \  (if a:actions(asig_of(D)) then                                            \
    8.78 -\     <snd(snd(snd(s))),a,snd(snd(snd(t)))>:trans_of(D)                      \
    8.79 +\     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
    8.80  \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
    8.81    by(simp_tac (SS addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
    8.82                              ioa_projections)
     9.1 --- a/src/HOL/IOA/meta_theory/IOA.thy	Thu Mar 23 15:39:13 1995 +0100
     9.2 +++ b/src/HOL/IOA/meta_theory/IOA.thy	Fri Mar 24 12:30:35 1995 +0100
     9.3 @@ -62,7 +62,7 @@
     9.4  state_trans_def
     9.5    "state_trans asig R == \
     9.6    \  (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \
     9.7 -  \  (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
     9.8 +  \  (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
     9.9  
    9.10  
    9.11  asig_of_def   "asig_of == fst"
    9.12 @@ -83,7 +83,7 @@
    9.13    "is_execution_fragment A ex ==                                        \
    9.14    \  let act = fst(ex); state = snd(ex)                                 \
    9.15    \  in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &              \
    9.16 -  \           (act(n)=Some(a) --> <state(n),a,state(Suc(n))>:trans_of(A))"
    9.17 +  \           (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
    9.18  
    9.19  
    9.20  executions_def
    9.21 @@ -98,7 +98,7 @@
    9.22   *      ----------------
    9.23   *      reachable(ioa,x)  
    9.24   *
    9.25 - *      reachable(ioa,s) & ? <s,a,s'>:trans_of(ioa)
    9.26 + *      reachable(ioa,s) & ? (s,a,s'):trans_of(ioa)
    9.27   *      -------------------------------------------
    9.28   *               reachable(ioa,s')
    9.29   *
    9.30 @@ -147,35 +147,35 @@
    9.31  
    9.32  asig_comp_def
    9.33    "asig_comp a1 a2 ==                                                   \
    9.34 -  \   (<(inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      \
    9.35 +  \   (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      \
    9.36    \     (outputs(a1) Un outputs(a2)),                                   \
    9.37 -  \     (internals(a1) Un internals(a2))>)"
    9.38 +  \     (internals(a1) Un internals(a2))))"
    9.39  
    9.40  
    9.41  par_def
    9.42    "(ioa1 || ioa2) ==                                                    \
    9.43 -  \    <asig_comp (asig_of ioa1) (asig_of ioa2),                        \
    9.44 +  \    (asig_comp (asig_of ioa1) (asig_of ioa2),                        \
    9.45    \     {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        \
    9.46    \     {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        \
    9.47    \          in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & \
    9.48    \             (if a:actions(asig_of(ioa1)) then                       \
    9.49 -  \                <fst(s),a,fst(t)>:trans_of(ioa1)                     \
    9.50 +  \                (fst(s),a,fst(t)):trans_of(ioa1)                     \
    9.51    \              else fst(t) = fst(s))                                  \
    9.52    \             &                                                       \
    9.53    \             (if a:actions(asig_of(ioa2)) then                       \
    9.54 -  \                <snd(s),a,snd(t)>:trans_of(ioa2)                     \
    9.55 -  \              else snd(t) = snd(s))}>"
    9.56 +  \                (snd(s),a,snd(t)):trans_of(ioa2)                     \
    9.57 +  \              else snd(t) = snd(s))})"
    9.58  
    9.59  
    9.60  restrict_asig_def
    9.61    "restrict_asig asig actns ==                                          \
    9.62 -\    <inputs(asig) Int actns, outputs(asig) Int actns,                  \
    9.63 -\     internals(asig) Un (externals(asig) - actns)>"
    9.64 +\    (inputs(asig) Int actns, outputs(asig) Int actns,                  \
    9.65 +\     internals(asig) Un (externals(asig) - actns))"
    9.66  
    9.67  
    9.68  restrict_def
    9.69    "restrict ioa actns ==                                               \
    9.70 -\    <restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa)>"
    9.71 +\    (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
    9.72  
    9.73  
    9.74  ioa_implements_def
    10.1 --- a/src/HOL/IOA/meta_theory/Solve.ML	Thu Mar 23 15:39:13 1995 +0100
    10.2 +++ b/src/HOL/IOA/meta_theory/Solve.ML	Fri Mar 24 12:30:35 1995 +0100
    10.3 @@ -18,7 +18,7 @@
    10.4    by (safe_tac set_cs);
    10.5  
    10.6    (* give execution of abstract automata *)
    10.7 -  by (res_inst_tac[("x","<mk_behaviour A (fst ex),%i.f(snd ex i)>")] bexI 1);
    10.8 +  by (res_inst_tac[("x","(mk_behaviour A (fst ex),%i.f(snd ex i))")] bexI 1);
    10.9  
   10.10    (* Behaviours coincide *)
   10.11    by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1);
    11.1 --- a/src/HOL/IOA/meta_theory/Solve.thy	Thu Mar 23 15:39:13 1995 +0100
    11.2 +++ b/src/HOL/IOA/meta_theory/Solve.thy	Fri Mar 24 12:30:35 1995 +0100
    11.3 @@ -18,9 +18,9 @@
    11.4    "is_weak_pmap f C A ==                          \
    11.5  \   (!s:starts_of(C). f(s):starts_of(A)) &        \
    11.6  \   (!s t a. reachable C s &                      \
    11.7 -\            <s,a,t>:trans_of(C)                  \
    11.8 +\            (s,a,t):trans_of(C)                  \
    11.9  \            --> (if a:externals(asig_of(C)) then \
   11.10 -\                   <f(s),a,f(t)>:trans_of(A)     \
   11.11 +\                   (f(s),a,f(t)):trans_of(A)     \
   11.12  \                 else f(s)=f(t)))"
   11.13  
   11.14  end
    12.1 --- a/src/HOL/Integ/Equiv.ML	Thu Mar 23 15:39:13 1995 +0100
    12.2 +++ b/src/HOL/Integ/Equiv.ML	Fri Mar 24 12:30:35 1995 +0100
    12.3 @@ -19,24 +19,24 @@
    12.4  by (fast_tac (comp_cs addSEs [converseD]) 1);
    12.5  qed "sym_trans_comp_subset";
    12.6  
    12.7 -val [major,minor]=goal Equiv.thy "[|<x,y>:r; z=<x,y>|] ==>  z:r";
    12.8 +val [major,minor]=goal Equiv.thy "[|(x,y):r; z=(x,y)|] ==>  z:r";
    12.9  by (simp_tac (prod_ss addsimps [minor]) 1);
   12.10  by (rtac major 1);
   12.11  qed "BreakPair";
   12.12  
   12.13 -val [major]=goal Equiv.thy "[|? x y. <x,y>:r & z=<x,y>|] ==>  z:r";
   12.14 +val [major]=goal Equiv.thy "[|? x y. (x,y):r & z=(x,y)|] ==>  z:r";
   12.15  by (resolve_tac [major RS exE] 1);
   12.16  by (etac exE 1);
   12.17  by (etac conjE 1);
   12.18  by (asm_simp_tac (prod_ss addsimps [minor]) 1);
   12.19  qed "BreakPair1";
   12.20  
   12.21 -val [major,minor]=goal Equiv.thy "[|z:r; z=<x,y>|] ==> <x,y>:r";
   12.22 +val [major,minor]=goal Equiv.thy "[|z:r; z=(x,y)|] ==> (x,y):r";
   12.23  by (simp_tac (prod_ss addsimps [minor RS sym]) 1);
   12.24  by (rtac major 1);
   12.25  qed "BuildPair";
   12.26  
   12.27 -val [major]=goal Equiv.thy "[|? z:r. <x,y>=z|] ==> <x,y>:r";
   12.28 +val [major]=goal Equiv.thy "[|? z:r. (x,y)=z|] ==> (x,y):r";
   12.29  by (resolve_tac [major RS bexE] 1);
   12.30  by (asm_simp_tac (prod_ss addsimps []) 1);
   12.31  qed "BuildPair1";
   12.32 @@ -65,7 +65,7 @@
   12.33  goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def]
   12.34      "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
   12.35  by (etac equalityE 1);
   12.36 -by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
   12.37 +by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
   12.38  by (safe_tac set_cs);
   12.39  by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3);
   12.40  by (fast_tac (set_cs addSIs [converseI] addIs [compI] addSEs [DomainE]) 2);
   12.41 @@ -84,14 +84,14 @@
   12.42  
   12.43  (*Lemma for the next result*)
   12.44  goalw Equiv.thy [equiv_def,trans_def,sym_def]
   12.45 -    "!!A r. [| equiv A r;  <a,b>: r |] ==> r^^{a} <= r^^{b}";
   12.46 +    "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
   12.47  by (safe_tac rel_cs);
   12.48  by (rtac ImageI 1);
   12.49  by (fast_tac rel_cs 2);
   12.50  by (fast_tac rel_cs 1);
   12.51  qed "equiv_class_subset";
   12.52  
   12.53 -goal Equiv.thy "!!A r. [| equiv A r;  <a,b>: r |] ==> r^^{a} = r^^{b}";
   12.54 +goal Equiv.thy "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
   12.55  by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
   12.56  by (rewrite_goals_tac [equiv_def,sym_def]);
   12.57  by (fast_tac rel_cs 1);
   12.58 @@ -105,18 +105,18 @@
   12.59  
   12.60  (*Lemma for the next result*)
   12.61  goalw Equiv.thy [equiv_def,refl_def]
   12.62 -    "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> <a,b>: r";
   12.63 +    "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
   12.64  by (fast_tac rel_cs 1);
   12.65  qed "subset_equiv_class";
   12.66  
   12.67  val prems = goal Equiv.thy
   12.68 -    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> <a,b>: r";
   12.69 +    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
   12.70  by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
   12.71  qed "eq_equiv_class";
   12.72  
   12.73  (*thus r^^{a} = r^^{b} as well*)
   12.74  goalw Equiv.thy [equiv_def,trans_def,sym_def]
   12.75 -    "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> <a,b>: r";
   12.76 +    "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
   12.77  by (fast_tac rel_cs 1);
   12.78  qed "equiv_class_nondisjoint";
   12.79  
   12.80 @@ -126,7 +126,7 @@
   12.81  qed "equiv_type";
   12.82  
   12.83  goal Equiv.thy
   12.84 -    "!!A r. equiv A r ==> (<x,y>: r) = (r^^{x} = r^^{y} & x:A & y:A)";
   12.85 +    "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
   12.86  by (safe_tac rel_cs);
   12.87  by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
   12.88  by ((rtac eq_equiv_class 3) THEN 
   12.89 @@ -138,7 +138,7 @@
   12.90  qed "equiv_class_eq_iff";
   12.91  
   12.92  goal Equiv.thy
   12.93 -    "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = (<x,y>: r)";
   12.94 +    "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
   12.95  by (safe_tac rel_cs);
   12.96  by ((rtac eq_equiv_class 1) THEN 
   12.97      (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
   12.98 @@ -227,7 +227,7 @@
   12.99  val _::_::prems = goalw Equiv.thy [quotient_def]
  12.100      "[| equiv A r;   congruent r b;  \
  12.101  \       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
  12.102 -\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] 	\
  12.103 +\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] 	\
  12.104  \    ==> X=Y";
  12.105  by (cut_facts_tac prems 1);
  12.106  by (safe_tac rel_cs);
  12.107 @@ -286,8 +286,8 @@
  12.108    than the direct proof*)
  12.109  val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def]
  12.110      "[| equiv A r;	\
  12.111 -\       !! y z w. [| w: A;  <y,z> : r |] ==> b y w = b z w;      \
  12.112 -\       !! y z w. [| w: A;  <y,z> : r |] ==> b w y = b w z       \
  12.113 +\       !! y z w. [| w: A;  (y,z) : r |] ==> b y w = b z w;      \
  12.114 +\       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
  12.115  \    |] ==> congruent2 r b";
  12.116  by (cut_facts_tac prems 1);
  12.117  by (safe_tac rel_cs);
  12.118 @@ -299,7 +299,7 @@
  12.119  val [equivA,commute,congt] = goal Equiv.thy
  12.120      "[| equiv A r;	\
  12.121  \       !! y z. [| y: A;  z: A |] ==> b y z = b z y;        \
  12.122 -\       !! y z w. [| w: A;  <y,z>: r |] ==> b w y = b w z	\
  12.123 +\       !! y z w. [| w: A;  (y,z): r |] ==> b w y = b w z	\
  12.124  \    |] ==> congruent2 r b";
  12.125  by (resolve_tac [equivA RS congruent2I] 1);
  12.126  by (rtac (commute RS trans) 1);
    13.1 --- a/src/HOL/Integ/Equiv.thy	Thu Mar 23 15:39:13 1995 +0100
    13.2 +++ b/src/HOL/Integ/Equiv.thy	Fri Mar 24 12:30:35 1995 +0100
    13.3 @@ -18,11 +18,11 @@
    13.4      congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
    13.5  
    13.6  defs
    13.7 -    refl_def      "refl A r == r <= Sigma A (%x.A) & (ALL x: A. <x,x> : r)"
    13.8 -    sym_def       "sym(r)    == ALL x y. <x,y>: r --> <y,x>: r"
    13.9 +    refl_def      "refl A r == r <= Sigma A (%x.A) & (ALL x: A. (x,x) : r)"
   13.10 +    sym_def       "sym(r)    == ALL x y. (x,y): r --> (y,x): r"
   13.11      equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
   13.12      quotient_def  "A/r == UN x:A. {r^^{x}}"  
   13.13 -    congruent_def   "congruent r b  == ALL y z. <y,z>:r --> b(y)=b(z)"
   13.14 +    congruent_def   "congruent r b  == ALL y z. (y,z):r --> b(y)=b(z)"
   13.15      congruent2_def  "congruent2 r b == ALL y1 z1 y2 z2. \
   13.16 -\           <y1,z1>:r --> <y2,z2>:r --> b y1 y2 = b z1 z2"
   13.17 +\           (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
   13.18  end
    14.1 --- a/src/HOL/Integ/Integ.ML	Thu Mar 23 15:39:13 1995 +0100
    14.2 +++ b/src/HOL/Integ/Integ.ML	Fri Mar 24 12:30:35 1995 +0100
    14.3 @@ -34,20 +34,20 @@
    14.4  
    14.5  val prems = goalw Integ.thy [intrel_def]
    14.6      "[| x1+y2 = x2+y1|] ==> \
    14.7 -\    <<x1,y1>,<x2,y2>>: intrel";
    14.8 +\    ((x1,y1),(x2,y2)): intrel";
    14.9  by (fast_tac (rel_cs addIs prems) 1);
   14.10  qed "intrelI";
   14.11  
   14.12  (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
   14.13  goalw Integ.thy [intrel_def]
   14.14    "p: intrel --> (EX x1 y1 x2 y2. \
   14.15 -\                  p = <<x1,y1>,<x2,y2>> & x1+y2 = x2+y1)";
   14.16 +\                  p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
   14.17  by (fast_tac rel_cs 1);
   14.18  qed "intrelE_lemma";
   14.19  
   14.20  val [major,minor] = goal Integ.thy
   14.21    "[| p: intrel;  \
   14.22 -\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1+y2 = x2+y1|] ==> Q |] \
   14.23 +\     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1|] ==> Q |] \
   14.24  \  ==> Q";
   14.25  by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
   14.26  by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
   14.27 @@ -55,11 +55,11 @@
   14.28  
   14.29  val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE];
   14.30  
   14.31 -goal Integ.thy "<<x1,y1>,<x2,y2>>: intrel = (x1+y2 = x2+y1)";
   14.32 +goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
   14.33  by (fast_tac intrel_cs 1);
   14.34  qed "intrel_iff";
   14.35  
   14.36 -goal Integ.thy "<x,x>: intrel";
   14.37 +goal Integ.thy "(x,x): intrel";
   14.38  by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1);
   14.39  qed "intrel_refl";
   14.40  
   14.41 @@ -74,7 +74,7 @@
   14.42      ([CollectI, CollectI] MRS 
   14.43      (equiv_intrel RS eq_equiv_class_iff));
   14.44  
   14.45 -goalw Integ.thy  [Integ_def,intrel_def,quotient_def] "intrel^^{<x,y>}:Integ";
   14.46 +goalw Integ.thy  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
   14.47  by (fast_tac set_cs 1);
   14.48  qed "intrel_in_integ";
   14.49  
   14.50 @@ -113,7 +113,7 @@
   14.51  (**** zminus: unary negation on Integ ****)
   14.52  
   14.53  goalw Integ.thy [congruent_def]
   14.54 -  "congruent intrel (%p. split (%x y. intrel^^{<y,x>}) p)";
   14.55 +  "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
   14.56  by (safe_tac intrel_cs);
   14.57  by (asm_simp_tac (intrel_ss addsimps add_ac) 1);
   14.58  qed "zminus_congruent";
   14.59 @@ -123,7 +123,7 @@
   14.60  val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   14.61  
   14.62  goalw Integ.thy [zminus_def]
   14.63 -      "$~ Abs_Integ(intrel^^{<x,y>}) = Abs_Integ(intrel ^^ {<y,x>})";
   14.64 +      "$~ Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
   14.65  by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
   14.66  by (simp_tac (set_ss addsimps 
   14.67     [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
   14.68 @@ -133,7 +133,7 @@
   14.69  
   14.70  (*by lcp*)
   14.71  val [prem] = goal Integ.thy
   14.72 -    "(!!x y. z = Abs_Integ(intrel^^{<x,y>}) ==> P) ==> P";
   14.73 +    "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
   14.74  by (res_inst_tac [("x1","z")] 
   14.75      (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
   14.76  by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
   14.77 @@ -202,7 +202,7 @@
   14.78  qed "diff_Suc_add_inverse";
   14.79  
   14.80  goalw Integ.thy [congruent_def]
   14.81 -    "congruent intrel (split (%x y. intrel^^{<(y-x) + (x-(y::nat)),0>}))";
   14.82 +    "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
   14.83  by (safe_tac intrel_cs);
   14.84  by (asm_simp_tac intrel_ss 1);
   14.85  by (etac rev_mp 1);
   14.86 @@ -225,8 +225,8 @@
   14.87  
   14.88  
   14.89  goalw Integ.thy [zmagnitude_def]
   14.90 -    "zmagnitude (Abs_Integ(intrel^^{<x,y>})) = \
   14.91 -\    Abs_Integ(intrel^^{<(y - x) + (x - y),0>})";
   14.92 +    "zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \
   14.93 +\    Abs_Integ(intrel^^{((y - x) + (x - y),0)})";
   14.94  by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
   14.95  by (asm_simp_tac (intrel_ss addsimps [zmagnitude_ize UN_equiv_class]) 1);
   14.96  qed "zmagnitude";
   14.97 @@ -246,7 +246,7 @@
   14.98  
   14.99  goalw Integ.thy [congruent2_def]
  14.100      "congruent2 intrel (%p1 p2.                  \
  14.101 -\         split (%x1 y1. split (%x2 y2. intrel^^{<x1+x2, y1+y2>}) p2) p1)";
  14.102 +\         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
  14.103  (*Proof via congruent2_commuteI seems longer*)
  14.104  by (safe_tac intrel_cs);
  14.105  by (asm_simp_tac (intrel_ss addsimps [add_assoc]) 1);
  14.106 @@ -260,8 +260,8 @@
  14.107  val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
  14.108  
  14.109  goalw Integ.thy [zadd_def]
  14.110 -  "Abs_Integ(intrel^^{<x1,y1>}) + Abs_Integ(intrel^^{<x2,y2>}) = \
  14.111 -\  Abs_Integ(intrel^^{<x1+x2, y1+y2>})";
  14.112 +  "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
  14.113 +\  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
  14.114  by (asm_simp_tac
  14.115      (intrel_ss addsimps [zadd_ize UN_equiv_class2]) 1);
  14.116  qed "zadd";
  14.117 @@ -333,7 +333,7 @@
  14.118  goal Integ.thy 
  14.119      "congruent2 intrel (%p1 p2.  		\
  14.120  \               split (%x1 y1. split (%x2 y2. 	\
  14.121 -\                   intrel^^{<x1*x2 + y1*y2, x1*y2 + y1*x2>}) p2) p1)";
  14.122 +\                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
  14.123  by (rtac (equiv_intrel RS congruent2_commuteI) 1);
  14.124  by (safe_tac intrel_cs);
  14.125  by (rewtac split_def);
  14.126 @@ -352,8 +352,8 @@
  14.127  val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
  14.128  
  14.129  goalw Integ.thy [zmult_def]
  14.130 -   "Abs_Integ((intrel^^{<x1,y1>})) * Abs_Integ((intrel^^{<x2,y2>})) = 	\
  14.131 -\   Abs_Integ(intrel ^^ {<x1*x2 + y1*y2, x1*y2 + y1*x2>})";
  14.132 +   "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = 	\
  14.133 +\   Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
  14.134  by (simp_tac (intrel_ss addsimps [zmult_ize UN_equiv_class2]) 1);
  14.135  qed "zmult";
  14.136  
    15.1 --- a/src/HOL/Integ/Integ.thy	Thu Mar 23 15:39:13 1995 +0100
    15.2 +++ b/src/HOL/Integ/Integ.thy	Fri Mar 24 12:30:35 1995 +0100
    15.3 @@ -14,7 +14,7 @@
    15.4  
    15.5  defs
    15.6    intrel_def
    15.7 -   "intrel == {p. ? x1 y1 x2 y2. p=<<x1::nat,y1>,<x2,y2>> & x1+y2 = x2+y1}"
    15.8 +   "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
    15.9  
   15.10  subtype (Integ)
   15.11    int = "{x::(nat*nat).True}/intrel"		("quotient_def")
   15.12 @@ -35,21 +35,21 @@
   15.13  defs
   15.14    zNat_def    "zNat == {x::nat. True}"
   15.15  
   15.16 -  znat_def    "$# m == Abs_Integ(intrel ^^ {<m,0>})"
   15.17 +  znat_def    "$# m == Abs_Integ(intrel ^^ {(m,0)})"
   15.18  
   15.19    zminus_def
   15.20 -	"$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{<y,x>}) p)"
   15.21 +	"$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
   15.22  
   15.23    znegative_def
   15.24 -      "znegative(Z) == EX x y. x<y & <x,y::nat>:Rep_Integ(Z)"
   15.25 +      "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
   15.26  
   15.27    zmagnitude_def
   15.28 -      "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{<(y-x) + (x-y),0>}) p)"
   15.29 +      "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
   15.30  
   15.31    zadd_def
   15.32     "Z1 + Z2 == \
   15.33  \       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).   \
   15.34 -\           split (%x1 y1. split (%x2 y2. intrel^^{<x1+x2, y1+y2>}) p2) p1)"
   15.35 +\           split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
   15.36  
   15.37    zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)"
   15.38  
   15.39 @@ -60,19 +60,19 @@
   15.40    zmult_def
   15.41     "Z1 * Z2 == \
   15.42  \       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
   15.43 -\           split (%x2 y2. intrel^^{<x1*x2 + y1*y2, x1*y2 + y1*x2>}) p2) p1)"
   15.44 +\           split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
   15.45  
   15.46    zdiv_def
   15.47     "Z1 zdiv Z2 ==   \
   15.48  \       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
   15.49 -\           split (%x2 y2. intrel^^{<(x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   \
   15.50 -\           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2)>}) p2) p1)"
   15.51 +\           split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   \
   15.52 +\           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
   15.53  
   15.54    zmod_def
   15.55     "Z1 zmod Z2 ==   \
   15.56  \       Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   \
   15.57 -\           split (%x2 y2. intrel^^{<(x1-y1)mod((x2-y2)+(y2-x2)),   \
   15.58 -\           (x1-y1)mod((x2-y2)+(x2-y2))>}) p2) p1)"
   15.59 +\           split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),   \
   15.60 +\           (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
   15.61  
   15.62    zsuc_def     "zsuc(Z) == Z + $# Suc(0)"
   15.63  
    16.1 --- a/src/HOL/Integ/Relation.ML	Thu Mar 23 15:39:13 1995 +0100
    16.2 +++ b/src/HOL/Integ/Relation.ML	Fri Mar 24 12:30:35 1995 +0100
    16.3 @@ -12,18 +12,18 @@
    16.4  
    16.5  open Relation;
    16.6  
    16.7 -goalw Relation.thy [converse_def] "!!a b r. <a,b>:r ==> <b,a>:converse(r)";
    16.8 +goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
    16.9  by (simp_tac prod_ss 1);
   16.10  by (fast_tac set_cs 1);
   16.11  qed "converseI";
   16.12  
   16.13 -goalw Relation.thy [converse_def] "!!a b r. <a,b> : converse(r) ==> <b,a> : r";
   16.14 +goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
   16.15  by (fast_tac comp_cs 1);
   16.16  qed "converseD";
   16.17  
   16.18  qed_goalw "converseE" Relation.thy [converse_def]
   16.19      "[| yx : converse(r);  \
   16.20 -\       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
   16.21 +\       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
   16.22  \    |] ==> P"
   16.23   (fn [major,minor]=>
   16.24    [ (rtac (major RS CollectE) 1),
   16.25 @@ -35,23 +35,23 @@
   16.26  			  addSEs [converseD,converseE];
   16.27  
   16.28  qed_goalw "Domain_iff" Relation.thy [Domain_def]
   16.29 -    "a: Domain(r) = (EX y. <a,y>: r)"
   16.30 +    "a: Domain(r) = (EX y. (a,y): r)"
   16.31   (fn _=> [ (fast_tac comp_cs 1) ]);
   16.32  
   16.33 -qed_goal "DomainI" Relation.thy "!!a b r. <a,b>: r ==> a: Domain(r)"
   16.34 +qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
   16.35   (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
   16.36  
   16.37  qed_goal "DomainE" Relation.thy
   16.38 -    "[| a : Domain(r);  !!y. <a,y>: r ==> P |] ==> P"
   16.39 +    "[| a : Domain(r);  !!y. (a,y): r ==> P |] ==> P"
   16.40   (fn prems=>
   16.41    [ (rtac (Domain_iff RS iffD1 RS exE) 1),
   16.42      (REPEAT (ares_tac prems 1)) ]);
   16.43  
   16.44 -qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.<a,b>: r ==> b : Range(r)"
   16.45 +qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
   16.46   (fn _ => [ (etac (converseI RS DomainI) 1) ]);
   16.47  
   16.48  qed_goalw "RangeE" Relation.thy [Range_def]
   16.49 -    "[| b : Range(r);  !!x. <x,b>: r ==> P |] ==> P"
   16.50 +    "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
   16.51   (fn major::prems=>
   16.52    [ (rtac (major RS DomainE) 1),
   16.53      (resolve_tac prems 1),
   16.54 @@ -60,23 +60,23 @@
   16.55  (*** Image of a set under a function/relation ***)
   16.56  
   16.57  qed_goalw "Image_iff" Relation.thy [Image_def]
   16.58 -    "b : r^^A = (? x:A. <x,b>:r)"
   16.59 +    "b : r^^A = (? x:A. (x,b):r)"
   16.60   (fn _ => [ fast_tac (comp_cs addIs [RangeI]) 1 ]);
   16.61  
   16.62  qed_goal "Image_singleton_iff" Relation.thy
   16.63 -    "(b : r^^{a}) = (<a,b>:r)"
   16.64 +    "(b : r^^{a}) = ((a,b):r)"
   16.65   (fn _ => [ rtac (Image_iff RS trans) 1,
   16.66  	    fast_tac comp_cs 1 ]);
   16.67  
   16.68  qed_goalw "ImageI" Relation.thy [Image_def]
   16.69 -    "!!a b r. [| <a,b>: r;  a:A |] ==> b : r^^A"
   16.70 +    "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
   16.71   (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
   16.72              (resolve_tac [conjI ] 1),
   16.73              (resolve_tac [RangeI] 1),
   16.74              (REPEAT (fast_tac set_cs 1))]);
   16.75  
   16.76  qed_goalw "ImageE" Relation.thy [Image_def]
   16.77 -    "[| b: r^^A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
   16.78 +    "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
   16.79   (fn major::prems=>
   16.80    [ (rtac (major RS CollectE) 1),
   16.81      (safe_tac set_cs),
    17.1 --- a/src/HOL/Integ/Relation.thy	Thu Mar 23 15:39:13 1995 +0100
    17.2 +++ b/src/HOL/Integ/Relation.thy	Fri Mar 24 12:30:35 1995 +0100
    17.3 @@ -16,9 +16,9 @@
    17.4      Range       ::      "('a*'a) set => 'a set"
    17.5  
    17.6  defs
    17.7 -    converse_def  "converse(r) == {z. (? w:r. ? x y. w=<x,y> & z=<y,x>)}"
    17.8 -    Domain_def    "Domain(r) == {z. ! x. (z=x --> (? y. <x,y>:r))}"
    17.9 +    converse_def  "converse(r) == {z. (? w:r. ? x y. w=(x,y) & z=(y,x))}"
   17.10 +    Domain_def    "Domain(r) == {z. ! x. (z=x --> (? y. (x,y):r))}"
   17.11      Range_def     "Range(r) == Domain(converse(r))"
   17.12 -    Image_def     "r ^^ s == {y. y:Range(r) &  (? x:s. <x,y>:r)}"
   17.13 +    Image_def     "r ^^ s == {y. y:Range(r) &  (? x:s. (x,y):r)}"
   17.14  
   17.15  end
    18.1 --- a/src/HOL/Nat.ML	Thu Mar 23 15:39:13 1995 +0100
    18.2 +++ b/src/HOL/Nat.ML	Fri Mar 24 12:30:35 1995 +0100
    18.3 @@ -136,12 +136,12 @@
    18.4  
    18.5  (** Introduction rules for 'pred_nat' **)
    18.6  
    18.7 -goalw Nat.thy [pred_nat_def] "<n, Suc(n)> : pred_nat";
    18.8 +goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
    18.9  by (fast_tac set_cs 1);
   18.10  qed "pred_natI";
   18.11  
   18.12  val major::prems = goalw Nat.thy [pred_nat_def]
   18.13 -    "[| p : pred_nat;  !!x n. [| p = <n, Suc(n)> |] ==> R \
   18.14 +    "[| p : pred_nat;  !!x n. [| p = (n, Suc(n)) |] ==> R \
   18.15  \    |] ==> R";
   18.16  by (rtac (major RS CollectE) 1);
   18.17  by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1));
   18.18 @@ -204,7 +204,7 @@
   18.19  by (rtac (pred_natI RS r_into_trancl) 1);
   18.20  qed "lessI";
   18.21  
   18.22 -(* i<j ==> i<Suc(j) *)
   18.23 +(* i(j ==> i(Suc(j) *)
   18.24  val less_SucI = lessI RSN (2, less_trans);
   18.25  
   18.26  goal Nat.thy "0 < Suc(n)";
   18.27 @@ -220,7 +220,7 @@
   18.28  by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
   18.29  qed "less_not_sym";
   18.30  
   18.31 -(* [| n<m; m<n |] ==> R *)
   18.32 +(* [| n(m; m(n |] ==> R *)
   18.33  bind_thm ("less_asym", (less_not_sym RS notE));
   18.34  
   18.35  goalw Nat.thy [less_def] "~ n<(n::nat)";
   18.36 @@ -228,7 +228,7 @@
   18.37  by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
   18.38  qed "less_not_refl";
   18.39  
   18.40 -(* n<n ==> R *)
   18.41 +(* n(n ==> R *)
   18.42  bind_thm ("less_anti_refl", (less_not_refl RS notE));
   18.43  
   18.44  goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
    19.1 --- a/src/HOL/Nat.thy	Thu Mar 23 15:39:13 1995 +0100
    19.2 +++ b/src/HOL/Nat.thy	Fri Mar 24 12:30:35 1995 +0100
    19.3 @@ -59,9 +59,9 @@
    19.4    (*nat operations and recursion*)
    19.5    nat_case_def  "nat_case a f n == @z.  (n=0 --> z=a)  \
    19.6  \                                        & (!x. n=Suc(x) --> z=f(x))"
    19.7 -  pred_nat_def  "pred_nat == {p. ? n. p = <n, Suc(n)>}"
    19.8 +  pred_nat_def  "pred_nat == {p. ? n. p = (n, Suc(n))}"
    19.9  
   19.10 -  less_def "m<n == <m,n>:trancl(pred_nat)"
   19.11 +  less_def "m<n == (m,n):trancl(pred_nat)"
   19.12  
   19.13    le_def   "m<=(n::nat) == ~(n<m)"
   19.14  
    20.1 --- a/src/HOL/Prod.ML	Thu Mar 23 15:39:13 1995 +0100
    20.2 +++ b/src/HOL/Prod.ML	Fri Mar 24 12:30:35 1995 +0100
    20.3 @@ -25,35 +25,35 @@
    20.4  qed "inj_onto_Abs_Prod";
    20.5  
    20.6  val prems = goalw Prod.thy [Pair_def]
    20.7 -    "[| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R";
    20.8 +    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
    20.9  by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1);
   20.10  by (REPEAT (ares_tac (prems@[ProdI]) 1));
   20.11  qed "Pair_inject";
   20.12  
   20.13 -goal Prod.thy "(<a,b> = <a',b'>) = (a=a' & b=b')";
   20.14 +goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
   20.15  by (fast_tac (set_cs addIs [Pair_inject]) 1);
   20.16  qed "Pair_eq";
   20.17  
   20.18 -goalw Prod.thy [fst_def] "fst(<a,b>) = a";
   20.19 +goalw Prod.thy [fst_def] "fst((a,b)) = a";
   20.20  by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
   20.21  qed "fst_conv";
   20.22  
   20.23 -goalw Prod.thy [snd_def] "snd(<a,b>) = b";
   20.24 +goalw Prod.thy [snd_def] "snd((a,b)) = b";
   20.25  by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1);
   20.26  qed "snd_conv";
   20.27  
   20.28 -goalw Prod.thy [Pair_def] "? x y. p = <x,y>";
   20.29 +goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
   20.30  by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
   20.31  by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
   20.32  	   rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
   20.33  qed "PairE_lemma";
   20.34  
   20.35 -val [prem] = goal Prod.thy "[| !!x y. p = <x,y> ==> Q |] ==> Q";
   20.36 +val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
   20.37  by (rtac (PairE_lemma RS exE) 1);
   20.38  by (REPEAT (eresolve_tac [prem,exE] 1));
   20.39  qed "PairE";
   20.40  
   20.41 -goalw Prod.thy [split_def] "split c <a,b> = c a b";
   20.42 +goalw Prod.thy [split_def] "split c (a,b) = c a b";
   20.43  by (sstac [fst_conv, snd_conv] 1);
   20.44  by (rtac refl 1);
   20.45  qed "split";
   20.46 @@ -72,18 +72,18 @@
   20.47    (fn [prem] => [rtac (prem RS arg_cong) 1]);
   20.48  
   20.49  (* Do not add as rewrite rule: invalidates some proofs in IMP *)
   20.50 -goal Prod.thy "p = <fst(p),snd(p)>";
   20.51 +goal Prod.thy "p = (fst(p),snd(p))";
   20.52  by (res_inst_tac [("p","p")] PairE 1);
   20.53  by (asm_simp_tac prod_ss 1);
   20.54  qed "surjective_pairing";
   20.55  
   20.56 -goal Prod.thy "p = split (%x y.<x,y>) p";
   20.57 +goal Prod.thy "p = split (%x y.(x,y)) p";
   20.58  by (res_inst_tac [("p","p")] PairE 1);
   20.59  by (asm_simp_tac prod_ss 1);
   20.60  qed "surjective_pairing2";
   20.61  
   20.62  (*For use with split_tac and the simplifier*)
   20.63 -goal Prod.thy "R(split c p) = (! x y. p = <x,y> --> R(c x y))";
   20.64 +goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
   20.65  by (stac surjective_pairing 1);
   20.66  by (stac split 1);
   20.67  by (fast_tac (HOL_cs addSEs [Pair_inject]) 1);
   20.68 @@ -94,31 +94,31 @@
   20.69  (*These rules are for use with fast_tac.
   20.70    Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
   20.71  
   20.72 -goal Prod.thy "!!a b c. c a b ==> split c <a,b>";
   20.73 +goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
   20.74  by (asm_simp_tac prod_ss 1);
   20.75  qed "splitI";
   20.76  
   20.77  val prems = goalw Prod.thy [split_def]
   20.78 -    "[| split c p;  !!x y. [| p = <x,y>;  c x y |] ==> Q |] ==> Q";
   20.79 +    "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
   20.80  by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   20.81  qed "splitE";
   20.82  
   20.83 -goal Prod.thy "!!R a b. split R <a,b> ==> R a b";
   20.84 +goal Prod.thy "!!R a b. split R (a,b) ==> R a b";
   20.85  by (etac (split RS iffD1) 1);
   20.86  qed "splitD";
   20.87  
   20.88 -goal Prod.thy "!!a b c. z: c a b ==> z: split c <a,b>";
   20.89 +goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
   20.90  by (asm_simp_tac prod_ss 1);
   20.91  qed "mem_splitI";
   20.92  
   20.93  val prems = goalw Prod.thy [split_def]
   20.94 -    "[| z: split c p;  !!x y. [| p = <x,y>;  z: c x y |] ==> Q |] ==> Q";
   20.95 +    "[| z: split c p;  !!x y. [| p = (x,y);  z: c x y |] ==> Q |] ==> Q";
   20.96  by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   20.97  qed "mem_splitE";
   20.98  
   20.99  (*** prod_fun -- action of the product functor upon functions ***)
  20.100  
  20.101 -goalw Prod.thy [prod_fun_def] "prod_fun f g <a,b> = <f(a),g(b)>";
  20.102 +goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
  20.103  by (rtac split 1);
  20.104  qed "prod_fun";
  20.105  
  20.106 @@ -135,14 +135,14 @@
  20.107  by (asm_simp_tac (prod_ss addsimps [prod_fun]) 1);
  20.108  qed "prod_fun_ident";
  20.109  
  20.110 -val prems = goal Prod.thy "<a,b>:r ==> <f(a),g(b)> : (prod_fun f g)``r";
  20.111 +val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
  20.112  by (rtac image_eqI 1);
  20.113  by (rtac (prod_fun RS sym) 1);
  20.114  by (resolve_tac prems 1);
  20.115  qed "prod_fun_imageI";
  20.116  
  20.117  val major::prems = goal Prod.thy
  20.118 -    "[| c: (prod_fun f g)``r;  !!x y. [| c=<f(x),g(y)>;  <x,y>:r |] ==> P  \
  20.119 +    "[| c: (prod_fun f g)``r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P  \
  20.120  \    |] ==> P";
  20.121  by (rtac (major RS imageE) 1);
  20.122  by (res_inst_tac [("p","x")] PairE 1);
  20.123 @@ -154,31 +154,31 @@
  20.124  (*** Disjoint union of a family of sets - Sigma ***)
  20.125  
  20.126  qed_goalw "SigmaI" Prod.thy [Sigma_def]
  20.127 -    "[| a:A;  b:B(a) |] ==> <a,b> : Sigma A B"
  20.128 +    "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
  20.129   (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
  20.130  
  20.131  (*The general elimination rule*)
  20.132  qed_goalw "SigmaE" Prod.thy [Sigma_def]
  20.133      "[| c: Sigma A B;  \
  20.134 -\       !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P \
  20.135 +\       !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P \
  20.136  \    |] ==> P"
  20.137   (fn major::prems=>
  20.138    [ (cut_facts_tac [major] 1),
  20.139      (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
  20.140  
  20.141 -(** Elimination of <a,b>:A*B -- introduces no eigenvariables **)
  20.142 -qed_goal "SigmaD1" Prod.thy "<a,b> : Sigma A B ==> a : A"
  20.143 +(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
  20.144 +qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
  20.145   (fn [major]=>
  20.146    [ (rtac (major RS SigmaE) 1),
  20.147      (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
  20.148  
  20.149 -qed_goal "SigmaD2" Prod.thy "<a,b> : Sigma A B ==> b : B(a)"
  20.150 +qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
  20.151   (fn [major]=>
  20.152    [ (rtac (major RS SigmaE) 1),
  20.153      (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
  20.154  
  20.155  qed_goal "SigmaE2" Prod.thy
  20.156 -    "[| <a,b> : Sigma A B;    \
  20.157 +    "[| (a,b) : Sigma A B;    \
  20.158  \       [| a:A;  b:B(a) |] ==> P   \
  20.159  \    |] ==> P"
  20.160   (fn [major,minor]=>
  20.161 @@ -188,7 +188,7 @@
  20.162  
  20.163  (*** Domain of a relation ***)
  20.164  
  20.165 -val prems = goalw Prod.thy [image_def] "<a,b> : r ==> a : fst``r";
  20.166 +val prems = goalw Prod.thy [image_def] "(a,b) : r ==> a : fst``r";
  20.167  by (rtac CollectI 1);
  20.168  by (rtac bexI 1);
  20.169  by (rtac (fst_conv RS sym) 1);
  20.170 @@ -196,7 +196,7 @@
  20.171  qed "fst_imageI";
  20.172  
  20.173  val major::prems = goal Prod.thy
  20.174 -    "[| a : fst``r;  !!y.[| <a,y> : r |] ==> P |] ==> P"; 
  20.175 +    "[| a : fst``r;  !!y.[| (a,y) : r |] ==> P |] ==> P"; 
  20.176  by (rtac (major RS imageE) 1);
  20.177  by (resolve_tac prems 1);
  20.178  by (etac ssubst 1);
  20.179 @@ -206,7 +206,7 @@
  20.180  
  20.181  (*** Range of a relation ***)
  20.182  
  20.183 -val prems = goalw Prod.thy [image_def] "<a,b> : r ==> b : snd``r";
  20.184 +val prems = goalw Prod.thy [image_def] "(a,b) : r ==> b : snd``r";
  20.185  by (rtac CollectI 1);
  20.186  by (rtac bexI 1);
  20.187  by (rtac (snd_conv RS sym) 1);
  20.188 @@ -214,7 +214,7 @@
  20.189  qed "snd_imageI";
  20.190  
  20.191  val major::prems = goal Prod.thy
  20.192 -    "[| a : snd``r;  !!y.[| <y,a> : r |] ==> P |] ==> P"; 
  20.193 +    "[| a : snd``r;  !!y.[| (y,a) : r |] ==> P |] ==> P"; 
  20.194  by (rtac (major RS imageE) 1);
  20.195  by (resolve_tac prems 1);
  20.196  by (etac ssubst 1);
  20.197 @@ -225,7 +225,7 @@
  20.198  (** Exhaustion rule for unit -- a degenerate form of induction **)
  20.199  
  20.200  goalw Prod.thy [Unity_def]
  20.201 -    "u = Unity";
  20.202 +    "u = ()";
  20.203  by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1);
  20.204  by (rtac (Rep_Unit_inverse RS sym) 1);
  20.205  qed "unit_eq";
    21.1 --- a/src/HOL/Prod.thy	Thu Mar 23 15:39:13 1995 +0100
    21.2 +++ b/src/HOL/Prod.thy	Fri Mar 24 12:30:35 1995 +0100
    21.3 @@ -35,20 +35,19 @@
    21.4    Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
    21.5  
    21.6  syntax
    21.7 -  "@Tuple"      :: "args => 'a * 'b"            ("(1<_>)")
    21.8 +  "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
    21.9  
   21.10  translations
   21.11 -  "<x, y, z>"   == "<x, <y, z>>"
   21.12 -  "<x, y>"      == "Pair x y"
   21.13 -  "<x>"         => "x"
   21.14 +  "(x, y, z)"   == "(x, (y, z))"
   21.15 +  "(x, y)"      == "Pair x y"
   21.16  
   21.17  defs
   21.18    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
   21.19 -  fst_def       "fst(p) == @a. ? b. p = <a, b>"
   21.20 -  snd_def       "snd(p) == @b. ? a. p = <a, b>"
   21.21 +  fst_def       "fst(p) == @a. ? b. p = (a, b)"
   21.22 +  snd_def       "snd(p) == @b. ? a. p = (a, b)"
   21.23    split_def     "split c p == c (fst p) (snd p)"
   21.24 -  prod_fun_def  "prod_fun f g == split(%x y.<f(x), g(y)>)"
   21.25 -  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {<x, y>}"
   21.26 +  prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
   21.27 +  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
   21.28  
   21.29  
   21.30  
   21.31 @@ -58,9 +57,9 @@
   21.32    unit = "{p. p = True}"
   21.33  
   21.34  consts
   21.35 -  Unity         :: "unit"                       ("'(')")
   21.36 +  "()"          :: "unit"                           ("'(')")
   21.37  
   21.38  defs
   21.39 -  Unity_def     "Unity == Abs_Unit(True)"
   21.40 +  Unity_def     "() == Abs_Unit(True)"
   21.41  
   21.42  end
    22.1 --- a/src/HOL/Sexp.ML	Thu Mar 23 15:39:13 1995 +0100
    22.2 +++ b/src/HOL/Sexp.ML	Fri Mar 24 12:30:35 1995 +0100
    22.3 @@ -63,19 +63,19 @@
    22.4  by (fast_tac sexp_cs 1);
    22.5  qed "pred_sexp_subset_Sigma";
    22.6  
    22.7 -(* <a,b> : pred_sexp^+ ==> a : sexp *)
    22.8 +(* (a,b) : pred_sexp^+ ==> a : sexp *)
    22.9  val trancl_pred_sexpD1 = 
   22.10      pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
   22.11  and trancl_pred_sexpD2 = 
   22.12      pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
   22.13  
   22.14  val prems = goalw Sexp.thy [pred_sexp_def]
   22.15 -    "[| M: sexp;  N: sexp |] ==> <M, M$N> : pred_sexp";
   22.16 +    "[| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
   22.17  by (fast_tac (set_cs addIs prems) 1);
   22.18  qed "pred_sexpI1";
   22.19  
   22.20  val prems = goalw Sexp.thy [pred_sexp_def]
   22.21 -    "[| M: sexp;  N: sexp |] ==> <N, M$N> : pred_sexp";
   22.22 +    "[| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
   22.23  by (fast_tac (set_cs addIs prems) 1);
   22.24  qed "pred_sexpI2";
   22.25  
   22.26 @@ -86,7 +86,7 @@
   22.27  val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
   22.28  and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
   22.29  
   22.30 -(*Proves goals of the form <M,N>:pred_sexp^+ provided M,N:sexp*)
   22.31 +(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
   22.32  val pred_sexp_simps =
   22.33              sexp.intrs @
   22.34  	    [pred_sexp_t1, pred_sexp_t2,
   22.35 @@ -95,8 +95,8 @@
   22.36  
   22.37  val major::prems = goalw Sexp.thy [pred_sexp_def]
   22.38      "[| p : pred_sexp;  \
   22.39 -\       !!M N. [| p = <M, M$N>;  M: sexp;  N: sexp |] ==> R; \
   22.40 -\       !!M N. [| p = <N, M$N>;  M: sexp;  N: sexp |] ==> R  \
   22.41 +\       !!M N. [| p = (M, M$N);  M: sexp;  N: sexp |] ==> R; \
   22.42 +\       !!M N. [| p = (N, M$N);  M: sexp;  N: sexp |] ==> R  \
   22.43  \    |] ==> R";
   22.44  by (cut_facts_tac [major] 1);
   22.45  by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
    23.1 --- a/src/HOL/Sexp.thy	Thu Mar 23 15:39:13 1995 +0100
    23.2 +++ b/src/HOL/Sexp.thy	Fri Mar 24 12:30:35 1995 +0100
    23.3 @@ -32,7 +32,7 @@
    23.4  \                           | (? N1 N2. M = N1 $ N2  & z=e N1 N2)"
    23.5  
    23.6    pred_sexp_def
    23.7 -     "pred_sexp == UN M: sexp. UN N: sexp. {<M, M$N>, <N, M$N>}"
    23.8 +     "pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
    23.9  
   23.10    sexp_rec_def
   23.11     "sexp_rec M c d e == wfrec pred_sexp M  \
    24.1 --- a/src/HOL/Subst/AList.ML	Thu Mar 23 15:39:13 1995 +0100
    24.2 +++ b/src/HOL/Subst/AList.ML	Fri Mar 24 12:30:35 1995 +0100
    24.3 @@ -12,13 +12,13 @@
    24.4                              (fn _ => [simp_tac list_ss 1])
    24.5    in map mk_thm 
    24.6       ["alist_rec [] c d = c",
    24.7 -      "alist_rec (<a,b>#al) c d = d a b al (alist_rec al c d)",
    24.8 +      "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)",
    24.9        "assoc v d [] = d",
   24.10 -      "assoc v d (<a,b>#al) = (if v=a then b else assoc v d al)"] end;
   24.11 +      "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] end;
   24.12  
   24.13  val prems = goal AList.thy
   24.14      "[| P([]);   \
   24.15 -\       !!x y xs. P(xs) ==> P(<x,y>#xs) |]  ==> P(l)";
   24.16 +\       !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)";
   24.17  by (list.induct_tac "l" 1);
   24.18  by (resolve_tac prems 1);
   24.19  by (rtac PairE 1);
    25.1 --- a/src/HOL/Subst/Subst.ML	Thu Mar 23 15:39:13 1995 +0100
    25.2 +++ b/src/HOL/Subst/Subst.ML	Fri Mar 24 12:30:35 1995 +0100
    25.3 @@ -19,9 +19,9 @@
    25.4  ["Const(c) <| al = Const(c)",
    25.5   "Comb t u <| al = Comb (t <| al) (u <| al)",
    25.6   "[] <> bl = bl",
    25.7 - "(<a,b>#al) <> bl = <a,b <| bl> # (al <> bl)",
    25.8 + "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
    25.9   "sdom([]) = {}",
   25.10 - "sdom(<a,b>#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \
   25.11 + "sdom((a,b)#al) = (if Var(a)=b then (sdom al) Int Compl({a}) \
   25.12  \                               else (sdom al) Un {a})"
   25.13  ];
   25.14     (* This rewrite isn't always desired *)
   25.15 @@ -42,10 +42,10 @@
   25.16  by (ALLGOALS (asm_simp_tac subst_ss));
   25.17  val subst_mono  = store_thm("subst_mono", result() RS mp);
   25.18  
   25.19 -goal Subst.thy  "~ (Var(v) <: t) --> t <| <v,t <| s>#s = t <| s";
   25.20 +goal Subst.thy  "~ (Var(v) <: t) --> t <| (v,t <| s)#s = t <| s";
   25.21  by (imp_excluded_middle_tac "t = Var(v)" 1);
   25.22  by (res_inst_tac [("P",
   25.23 -    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| <v,t<|s>#s=x<|s")]
   25.24 +    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
   25.25      uterm_induct 2);
   25.26  by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
   25.27  by (fast_tac HOL_cs 1);
   25.28 @@ -59,13 +59,13 @@
   25.29  by (ALLGOALS (fast_tac HOL_cs));
   25.30  qed "agreement";
   25.31  
   25.32 -goal Subst.thy   "~ v: vars_of(t) --> t <| <v,u>#s = t <| s";
   25.33 +goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
   25.34  by(simp_tac(subst_ss addsimps [agreement,Var_subst]
   25.35                       setloop (split_tac [expand_if])) 1);
   25.36  val repl_invariance  = store_thm("repl_invariance", result() RS mp);
   25.37  
   25.38  val asms = goal Subst.thy 
   25.39 -     "v : vars_of(t) --> w : vars_of(t <| <v,Var(w)>#s)";
   25.40 +     "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)";
   25.41  by (uterm_ind_tac "t" 1);
   25.42  by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
   25.43  val Var_in_subst  = store_thm("Var_in_subst", result() RS mp);
   25.44 @@ -113,7 +113,7 @@
   25.45  by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
   25.46  qed "comp_assoc";
   25.47  
   25.48 -goal Subst.thy "<w,Var(w) <| s>#s =s= s"; 
   25.49 +goal Subst.thy "(w,Var(w) <| s)#s =s= s"; 
   25.50  by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
   25.51  by (uterm_ind_tac "t" 1);
   25.52  by (REPEAT (etac rev_mp 3));
    26.1 --- a/src/HOL/Subst/Subst.thy	Thu Mar 23 15:39:13 1995 +0100
    26.2 +++ b/src/HOL/Subst/Subst.thy	Fri Mar 24 12:30:35 1995 +0100
    26.3 @@ -26,7 +26,7 @@
    26.4  \                         (%x.Const(x))			\
    26.5  \                         (%u v q r.Comb q r)"
    26.6  
    26.7 -  comp_def     "al <> bl == alist_rec al bl (%x y xs g.<x,y <| bl>#g)"
    26.8 +  comp_def     "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
    26.9  
   26.10    sdom_def
   26.11    "sdom(al) == alist_rec al {}  \
    27.1 --- a/src/HOL/Subst/Unifier.ML	Thu Mar 23 15:39:13 1995 +0100
    27.2 +++ b/src/HOL/Subst/Unifier.ML	Fri Mar 24 12:30:35 1995 +0100
    27.3 @@ -25,7 +25,7 @@
    27.4  
    27.5  goal Unifier.thy
    27.6    "~v : vars_of(t) --> ~v : vars_of(u) -->Unifier s t u --> \
    27.7 -\  Unifier (<v,r>#s) t u";
    27.8 +\  Unifier ((v,r)#s) t u";
    27.9  by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
   27.10  val Cons_Unifier  = store_thm("Cons_Unifier", result() RS mp RS mp RS mp);
   27.11  
   27.12 @@ -49,7 +49,7 @@
   27.13  qed "MGU_iff";
   27.14  
   27.15  val [prem] = goal Unifier.thy
   27.16 -     "~ Var(v) <: t ==> MGUnifier [<v,t>] (Var v) t";
   27.17 +     "~ Var(v) <: t ==> MGUnifier [(v,t)] (Var v) t";
   27.18  by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1);
   27.19  by (REPEAT_SOME (step_tac set_cs));
   27.20  by (etac subst 1);
   27.21 @@ -85,7 +85,7 @@
   27.22  by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
   27.23  qed "Idem_Nil";
   27.24  
   27.25 -goal Unifier.thy "~ (Var(v) <: t) --> Idem([<v,t>])";
   27.26 +goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
   27.27  by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
   27.28                         setloop (split_tac [expand_if])) 1);
   27.29  by (fast_tac set_cs 1);
   27.30 @@ -114,8 +114,8 @@
   27.31  
   27.32  val prems = goal Unifier.thy 
   27.33      "x : sdom(s) -->  ~x : srange(s) --> \
   27.34 -\   ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \
   27.35 -\      vars_of(Var(x) <| <x,Var(x)>#s)";
   27.36 +\   ~vars_of(Var(x) <| s<> (x,Var(x))#s) = \
   27.37 +\      vars_of(Var(x) <| (x,Var(x))#s)";
   27.38  by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
   27.39  by (REPEAT (resolve_tac [impI,disjI2] 1));
   27.40  by(res_inst_tac [("x","x")] exI 1);
   27.41 @@ -141,8 +141,8 @@
   27.42  
   27.43  val prems = goal Unifier.thy 
   27.44     "~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
   27.45 -\   ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \
   27.46 -\   vars_of(Var(w) <| <x,Var(w)>#s)";
   27.47 +\   ~vars_of(Var(w) <| s<> (x,Var(w))#s) = \
   27.48 +\   vars_of(Var(w) <| (x,Var(w))#s)";
   27.49  by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
   27.50  by (REPEAT (resolve_tac [impI,disjI1] 1));
   27.51  by(res_inst_tac [("x","w")] exI 1);
   27.52 @@ -167,10 +167,10 @@
   27.53  (*                                                                           *)
   27.54  (*  fun unify Const(m) Const(n) = if m=n then Nil else Fail                  *)
   27.55  (*    | unify Const(m) _        = Fail                                       *)
   27.56 -(*    | unify Var(v)   t        = if Var(v)<:t then Fail else <v,t>#Nil      *)
   27.57 +(*    | unify Var(v)   t        = if Var(v)<:t then Fail else (v,t)#Nil      *)
   27.58  (*    | unify Comb(t,u) Const(n) = Fail                                      *)
   27.59  (*    | unify Comb(t,u) Var(v)  = if Var(v) <: Comb(t,u) then Fail           *)
   27.60 -(*                                               else <v,Comb(t,u>#Nil       *)
   27.61 +(*                                               else (v,Comb(t,u)#Nil       *)
   27.62  (*    | unify Comb(t,u) Comb(v,w) = let s = unify t v                        *)
   27.63  (*                                  in if s=Fail then Fail                   *)
   27.64  (*                                               else unify (u<|s) (w<|s);   *)
   27.65 @@ -191,7 +191,7 @@
   27.66  val Unify2 = store_thm("Unify2", result() RS mp);
   27.67  
   27.68  val [prem] = goalw Unifier.thy [MGIUnifier_def] 
   27.69 - "~Var(v) <: t ==> MGIUnifier [<v,t>] (Var v) t";
   27.70 + "~Var(v) <: t ==> MGIUnifier [(v,t)] (Var v) t";
   27.71  by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
   27.72  qed "Unify3";
   27.73  
    28.1 --- a/src/HOL/Trancl.ML	Thu Mar 23 15:39:13 1995 +0100
    28.2 +++ b/src/HOL/Trancl.ML	Fri Mar 24 12:30:35 1995 +0100
    28.3 @@ -11,55 +11,55 @@
    28.4  (** Natural deduction for trans(r) **)
    28.5  
    28.6  val prems = goalw Trancl.thy [trans_def]
    28.7 -    "(!! x y z. [| <x,y>:r;  <y,z>:r |] ==> <x,z>:r) ==> trans(r)";
    28.8 +    "(!! x y z. [| (x,y):r;  (y,z):r |] ==> (x,z):r) ==> trans(r)";
    28.9  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
   28.10  qed "transI";
   28.11  
   28.12  val major::prems = goalw Trancl.thy [trans_def]
   28.13 -    "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
   28.14 +    "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
   28.15  by (cut_facts_tac [major] 1);
   28.16  by (fast_tac (HOL_cs addIs prems) 1);
   28.17  qed "transD";
   28.18  
   28.19  (** Identity relation **)
   28.20  
   28.21 -goalw Trancl.thy [id_def] "<a,a> : id";  
   28.22 +goalw Trancl.thy [id_def] "(a,a) : id";  
   28.23  by (rtac CollectI 1);
   28.24  by (rtac exI 1);
   28.25  by (rtac refl 1);
   28.26  qed "idI";
   28.27  
   28.28  val major::prems = goalw Trancl.thy [id_def]
   28.29 -    "[| p: id;  !!x.[| p = <x,x> |] ==> P  \
   28.30 +    "[| p: id;  !!x.[| p = (x,x) |] ==> P  \
   28.31  \    |] ==>  P";  
   28.32  by (rtac (major RS CollectE) 1);
   28.33  by (etac exE 1);
   28.34  by (eresolve_tac prems 1);
   28.35  qed "idE";
   28.36  
   28.37 -goalw Trancl.thy [id_def] "<a,b>:id = (a=b)";
   28.38 +goalw Trancl.thy [id_def] "(a,b):id = (a=b)";
   28.39  by(fast_tac prod_cs 1);
   28.40  qed "pair_in_id_conv";
   28.41  
   28.42  (** Composition of two relations **)
   28.43  
   28.44  val prems = goalw Trancl.thy [comp_def]
   28.45 -    "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
   28.46 +    "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
   28.47  by (fast_tac (set_cs addIs prems) 1);
   28.48  qed "compI";
   28.49  
   28.50  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
   28.51  val prems = goalw Trancl.thy [comp_def]
   28.52      "[| xz : r O s;  \
   28.53 -\       !!x y z. [| xz = <x,z>;  <x,y>:s;  <y,z>:r |] ==> P \
   28.54 +\       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
   28.55  \    |] ==> P";
   28.56  by (cut_facts_tac prems 1);
   28.57  by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
   28.58  qed "compE";
   28.59  
   28.60  val prems = goal Trancl.thy
   28.61 -    "[| <a,c> : r O s;  \
   28.62 -\       !!y. [| <a,y>:s;  <y,c>:r |] ==> P \
   28.63 +    "[| (a,c) : r O s;  \
   28.64 +\       !!y. [| (a,y):s;  (y,c):r |] ==> P \
   28.65  \    |] ==> P";
   28.66  by (rtac compE 1);
   28.67  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
   28.68 @@ -88,20 +88,20 @@
   28.69  val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
   28.70  
   28.71  (*Reflexivity of rtrancl*)
   28.72 -goal Trancl.thy "<a,a> : r^*";
   28.73 +goal Trancl.thy "(a,a) : r^*";
   28.74  by (stac rtrancl_unfold 1);
   28.75  by (fast_tac comp_cs 1);
   28.76  qed "rtrancl_refl";
   28.77  
   28.78  (*Closure under composition with r*)
   28.79  val prems = goal Trancl.thy
   28.80 -    "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
   28.81 +    "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
   28.82  by (stac rtrancl_unfold 1);
   28.83  by (fast_tac (comp_cs addIs prems) 1);
   28.84  qed "rtrancl_into_rtrancl";
   28.85  
   28.86  (*rtrancl of r contains r*)
   28.87 -val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*";
   28.88 +val [prem] = goal Trancl.thy "[| (a,b) : r |] ==> (a,b) : r^*";
   28.89  by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
   28.90  by (rtac prem 1);
   28.91  qed "r_into_rtrancl";
   28.92 @@ -114,22 +114,22 @@
   28.93  (** standard induction rule **)
   28.94  
   28.95  val major::prems = goal Trancl.thy 
   28.96 -  "[| <a,b> : r^*; \
   28.97 -\     !!x. P(<x,x>); \
   28.98 -\     !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |] \
   28.99 -\  ==>  P(<a,b>)";
  28.100 +  "[| (a,b) : r^*; \
  28.101 +\     !!x. P((x,x)); \
  28.102 +\     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
  28.103 +\  ==>  P((a,b))";
  28.104  by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
  28.105  by (fast_tac (comp_cs addIs prems) 1);
  28.106  qed "rtrancl_full_induct";
  28.107  
  28.108  (*nice induction rule*)
  28.109  val major::prems = goal Trancl.thy
  28.110 -    "[| <a::'a,b> : r^*;    \
  28.111 +    "[| (a::'a,b) : r^*;    \
  28.112  \       P(a); \
  28.113 -\	!!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z) |]  \
  28.114 +\	!!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
  28.115  \     ==> P(b)";
  28.116  (*by induction on this formula*)
  28.117 -by (subgoal_tac "! y. <a::'a,b> = <a,y> --> P(y)" 1);
  28.118 +by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
  28.119  (*now solve first subgoal: this formula is sufficient*)
  28.120  by (fast_tac HOL_cs 1);
  28.121  (*now do the induction*)
  28.122 @@ -147,10 +147,10 @@
  28.123  
  28.124  (*elimination of rtrancl -- by induction on a special formula*)
  28.125  val major::prems = goal Trancl.thy
  28.126 -    "[| <a::'a,b> : r^*;  (a = b) ==> P; 	\
  28.127 -\	!!y.[| <a,y> : r^*; <y,b> : r |] ==> P 	\
  28.128 +    "[| (a::'a,b) : r^*;  (a = b) ==> P; 	\
  28.129 +\	!!y.[| (a,y) : r^*; (y,b) : r |] ==> P 	\
  28.130  \    |] ==> P";
  28.131 -by (subgoal_tac "(a::'a) = b  | (? y. <a,y> : r^* & <y,b> : r)" 1);
  28.132 +by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
  28.133  by (rtac (major RS rtrancl_induct) 2);
  28.134  by (fast_tac (set_cs addIs prems) 2);
  28.135  by (fast_tac (set_cs addIs prems) 2);
  28.136 @@ -163,26 +163,26 @@
  28.137  (** Conversions between trancl and rtrancl **)
  28.138  
  28.139  val [major] = goalw Trancl.thy [trancl_def]
  28.140 -    "<a,b> : r^+ ==> <a,b> : r^*";
  28.141 +    "(a,b) : r^+ ==> (a,b) : r^*";
  28.142  by (resolve_tac [major RS compEpair] 1);
  28.143  by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
  28.144  qed "trancl_into_rtrancl";
  28.145  
  28.146  (*r^+ contains r*)
  28.147  val [prem] = goalw Trancl.thy [trancl_def]
  28.148 -   "[| <a,b> : r |] ==> <a,b> : r^+";
  28.149 +   "[| (a,b) : r |] ==> (a,b) : r^+";
  28.150  by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
  28.151  qed "r_into_trancl";
  28.152  
  28.153  (*intro rule by definition: from rtrancl and r*)
  28.154  val prems = goalw Trancl.thy [trancl_def]
  28.155 -    "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
  28.156 +    "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
  28.157  by (REPEAT (resolve_tac ([compI]@prems) 1));
  28.158  qed "rtrancl_into_trancl1";
  28.159  
  28.160  (*intro rule from r and rtrancl*)
  28.161  val prems = goal Trancl.thy
  28.162 -    "[| <a,b> : r;  <b,c> : r^* |]   ==>  <a,c> : r^+";
  28.163 +    "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
  28.164  by (resolve_tac (prems RL [rtranclE]) 1);
  28.165  by (etac subst 1);
  28.166  by (resolve_tac (prems RL [r_into_trancl]) 1);
  28.167 @@ -192,11 +192,11 @@
  28.168  
  28.169  (*elimination of r^+ -- NOT an induction rule*)
  28.170  val major::prems = goal Trancl.thy
  28.171 -    "[| <a::'a,b> : r^+;  \
  28.172 -\       <a,b> : r ==> P; \
  28.173 -\	!!y.[| <a,y> : r^+;  <y,b> : r |] ==> P  \
  28.174 +    "[| (a::'a,b) : r^+;  \
  28.175 +\       (a,b) : r ==> P; \
  28.176 +\	!!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
  28.177  \    |] ==> P";
  28.178 -by (subgoal_tac "<a::'a,b> : r | (? y. <a,y> : r^+  &  <y,b> : r)" 1);
  28.179 +by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
  28.180  by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
  28.181  by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
  28.182  by (etac rtranclE 1);
  28.183 @@ -214,7 +214,7 @@
  28.184  qed "trans_trancl";
  28.185  
  28.186  val prems = goal Trancl.thy
  28.187 -    "[| <a,b> : r;  <b,c> : r^+ |]   ==>  <a,c> : r^+";
  28.188 +    "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+";
  28.189  by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
  28.190  by (resolve_tac prems 1);
  28.191  by (resolve_tac prems 1);
  28.192 @@ -222,7 +222,7 @@
  28.193  
  28.194  
  28.195  val major::prems = goal Trancl.thy
  28.196 -    "[| <a,b> : r^*;  r <= Sigma A (%x.A) |] ==> a=b | a:A";
  28.197 +    "[| (a,b) : r^*;  r <= Sigma A (%x.A) |] ==> a=b | a:A";
  28.198  by (cut_facts_tac prems 1);
  28.199  by (rtac (major RS rtrancl_induct) 1);
  28.200  by (rtac (refl RS disjI1) 1);
    29.1 --- a/src/HOL/Trancl.thy	Thu Mar 23 15:39:13 1995 +0100
    29.2 +++ b/src/HOL/Trancl.thy	Fri Mar 24 12:30:35 1995 +0100
    29.3 @@ -16,11 +16,11 @@
    29.4      trancl  :: "('a * 'a)set => ('a * 'a)set"	("(_^+)" [100] 100)  
    29.5      O	    :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
    29.6  defs   
    29.7 -trans_def	"trans(r) == (!x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)"
    29.8 +trans_def	"trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
    29.9  comp_def	(*composition of relations*)
   29.10 -		"r O s == {xz. ? x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"
   29.11 +		"r O s == {xz. ? x y z. xz = (x,z) & (x,y):s & (y,z):r}"
   29.12  id_def		(*the identity relation*)
   29.13 -		"id == {p. ? x. p = <x,x>}"
   29.14 +		"id == {p. ? x. p = (x,x)}"
   29.15  rtrancl_def	"r^* == lfp(%s. id Un (r O s))"
   29.16  trancl_def	"r^+ == r O rtrancl(r)"
   29.17  end
    30.1 --- a/src/HOL/Univ.ML	Thu Mar 23 15:39:13 1995 +0100
    30.2 +++ b/src/HOL/Univ.ML	Fri Mar 24 12:30:35 1995 +0100
    30.3 @@ -51,12 +51,12 @@
    30.4  
    30.5  (** apfst -- can be used in similar type definitions **)
    30.6  
    30.7 -goalw Univ.thy [apfst_def] "apfst f <a,b> = <f(a),b>";
    30.8 +goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)";
    30.9  by (rtac split 1);
   30.10  qed "apfst";
   30.11  
   30.12  val [major,minor] = goal Univ.thy
   30.13 -    "[| q = apfst f p;  !!x y. [| p = <x,y>;  q = <f(x),y> |] ==> R \
   30.14 +    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R \
   30.15  \    |] ==> R";
   30.16  by (rtac PairE 1);
   30.17  by (rtac minor 1);
   30.18 @@ -109,7 +109,7 @@
   30.19  
   30.20  (*** Introduction rules for Node ***)
   30.21  
   30.22 -goalw Univ.thy [Node_def] "<%k. 0,a> : Node";
   30.23 +goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
   30.24  by (fast_tac set_cs 1);
   30.25  qed "Node_K0_I";
   30.26  
   30.27 @@ -256,7 +256,7 @@
   30.28  val univ_ss = nat_ss addsimps univ_simps;
   30.29  
   30.30  
   30.31 -goalw Univ.thy [ndepth_def] "ndepth (Abs_Node(<%k.0, x>)) = 0";
   30.32 +goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
   30.33  by (sstac [Node_K0_I RS Abs_Node_inverse, split] 1);
   30.34  by (rtac Least_equality 1);
   30.35  by (rtac refl 1);
   30.36 @@ -496,7 +496,7 @@
   30.37  
   30.38  (*** Equality : the diagonal relation ***)
   30.39  
   30.40 -goalw Univ.thy [diag_def] "!!a A. [| a=b;  a:A |] ==> <a,b> : diag(A)";
   30.41 +goalw Univ.thy [diag_def] "!!a A. [| a=b;  a:A |] ==> (a,b) : diag(A)";
   30.42  by (fast_tac set_cs 1);
   30.43  qed "diag_eqI";
   30.44  
   30.45 @@ -505,7 +505,7 @@
   30.46  (*The general elimination rule*)
   30.47  val major::prems = goalw Univ.thy [diag_def]
   30.48      "[| c : diag(A);  \
   30.49 -\       !!x y. [| x:A;  c = <x,x> |] ==> P \
   30.50 +\       !!x y. [| x:A;  c = (x,x) |] ==> P \
   30.51  \    |] ==> P";
   30.52  by (rtac (major RS UN_E) 1);
   30.53  by (REPEAT (eresolve_tac [asm_rl,singletonE] 1 ORELSE resolve_tac prems 1));
   30.54 @@ -514,14 +514,14 @@
   30.55  (*** Equality for Cartesian Product ***)
   30.56  
   30.57  goalw Univ.thy [dprod_def]
   30.58 -    "!!r s. [| <M,M'>:r;  <N,N'>:s |] ==> <M$N, M'$N'> : r<**>s";
   30.59 +    "!!r s. [| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
   30.60  by (fast_tac prod_cs 1);
   30.61  qed "dprodI";
   30.62  
   30.63  (*The general elimination rule*)
   30.64  val major::prems = goalw Univ.thy [dprod_def]
   30.65      "[| c : r<**>s;  \
   30.66 -\       !!x y x' y'. [| <x,x'> : r;  <y,y'> : s;  c = <x$y,x'$y'> |] ==> P \
   30.67 +\       !!x y x' y'. [| (x,x') : r;  (y,y') : s;  c = (x$y,x'$y') |] ==> P \
   30.68  \    |] ==> P";
   30.69  by (cut_facts_tac [major] 1);
   30.70  by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE]));
   30.71 @@ -531,18 +531,18 @@
   30.72  
   30.73  (*** Equality for Disjoint Sum ***)
   30.74  
   30.75 -goalw Univ.thy [dsum_def]  "!!r. <M,M'>:r ==> <In0(M), In0(M')> : r<++>s";
   30.76 +goalw Univ.thy [dsum_def]  "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
   30.77  by (fast_tac prod_cs 1);
   30.78  qed "dsum_In0I";
   30.79  
   30.80 -goalw Univ.thy [dsum_def]  "!!r. <N,N'>:s ==> <In1(N), In1(N')> : r<++>s";
   30.81 +goalw Univ.thy [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
   30.82  by (fast_tac prod_cs 1);
   30.83  qed "dsum_In1I";
   30.84  
   30.85  val major::prems = goalw Univ.thy [dsum_def]
   30.86      "[| w : r<++>s;  \
   30.87 -\       !!x x'. [| <x,x'> : r;  w = <In0(x), In0(x')> |] ==> P; \
   30.88 -\       !!y y'. [| <y,y'> : s;  w = <In1(y), In1(y')> |] ==> P \
   30.89 +\       !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P; \
   30.90 +\       !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P \
   30.91  \    |] ==> P";
   30.92  by (cut_facts_tac [major] 1);
   30.93  by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE]));
    31.1 --- a/src/HOL/Univ.thy	Thu Mar 23 15:39:13 1995 +0100
    31.2 +++ b/src/HOL/Univ.thy	Fri Mar 24 12:30:35 1995 +0100
    31.3 @@ -16,7 +16,7 @@
    31.4  (** lists, trees will be sets of nodes **)
    31.5  
    31.6  subtype (Node)
    31.7 -  'a node = "{p. EX f x k. p = <f::nat=>nat, x::'a+nat> & f(k)=0}"
    31.8 +  'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
    31.9  
   31.10  types
   31.11    'a item = "'a node set"
   31.12 @@ -58,13 +58,13 @@
   31.13    Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
   31.14  
   31.15    (*crude "lists" of nats -- needed for the constructions*)
   31.16 -  apfst_def  "apfst == (%f. split(%x y. <f(x),y>))"
   31.17 +  apfst_def  "apfst == (%f. split(%x y. (f(x),y)))"
   31.18    Push_def   "Push == (%b h. nat_case (Suc b) h)"
   31.19  
   31.20    (** operations on S-expressions -- sets of nodes **)
   31.21  
   31.22    (*S-expression constructors*)
   31.23 -  Atom_def   "Atom == (%x. {Abs_Node(<%k.0, x>)})"
   31.24 +  Atom_def   "Atom == (%x. {Abs_Node((%k.0, x))})"
   31.25    Scons_def  "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
   31.26  
   31.27    (*Leaf nodes, with arbitrary or nat labels*)
   31.28 @@ -92,12 +92,12 @@
   31.29  
   31.30    (** diagonal sets and equality for the "universe" **)
   31.31  
   31.32 -  diag_def   "diag(A) == UN x:A. {<x,x>}"
   31.33 +  diag_def   "diag(A) == UN x:A. {(x,x)}"
   31.34  
   31.35    dprod_def  "r<**>s == UN u:r. split (%x x'. \
   31.36 -\                       UN v:s. split (%y y'. {<x$y,x'$y'>}) v) u"
   31.37 +\                       UN v:s. split (%y y'. {(x$y,x'$y')}) v) u"
   31.38  
   31.39 -  dsum_def   "r<++>s == (UN u:r. split (%x x'. {<In0(x),In0(x')>}) u) Un \
   31.40 -\                       (UN v:s. split (%y y'. {<In1(y),In1(y')>}) v)"
   31.41 +  dsum_def   "r<++>s == (UN u:r. split (%x x'. {(In0(x),In0(x'))}) u) Un \
   31.42 +\                       (UN v:s. split (%y y'. {(In1(y),In1(y'))}) v)"
   31.43  
   31.44  end
    32.1 --- a/src/HOL/WF.ML	Thu Mar 23 15:39:13 1995 +0100
    32.2 +++ b/src/HOL/WF.ML	Fri Mar 24 12:30:35 1995 +0100
    32.3 @@ -14,7 +14,7 @@
    32.4  (*Restriction to domain A.  If r is well-founded over A then wf(r)*)
    32.5  val [prem1,prem2] = goalw WF.thy [wf_def]
    32.6   "[| r <= Sigma A (%u.A);  \
    32.7 -\    !!x P. [| ! x. (! y. <y,x> : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
    32.8 +\    !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
    32.9  \ ==>  wf(r)";
   32.10  by (strip_tac 1);
   32.11  by (rtac allE 1);
   32.12 @@ -24,7 +24,7 @@
   32.13  
   32.14  val major::prems = goalw WF.thy [wf_def]
   32.15      "[| wf(r);          \
   32.16 -\       !!x.[| ! y. <y,x>: r --> P(y) |] ==> P(x) \
   32.17 +\       !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
   32.18  \    |]  ==>  P(a)";
   32.19  by (rtac (major RS spec RS mp RS spec) 1);
   32.20  by (fast_tac (HOL_cs addEs prems) 1);
   32.21 @@ -36,14 +36,14 @@
   32.22  	   rename_last_tac a ["1"] (i+1),
   32.23  	   ares_tac prems i];
   32.24  
   32.25 -val prems = goal WF.thy "[| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
   32.26 -by (subgoal_tac "! x. <a,x>:r --> <x,a>:r --> P" 1);
   32.27 +val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
   32.28 +by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
   32.29  by (fast_tac (HOL_cs addIs prems) 1);
   32.30  by (wf_ind_tac "a" prems 1);
   32.31  by (fast_tac set_cs 1);
   32.32  qed "wf_asym";
   32.33  
   32.34 -val prems = goal WF.thy "[| wf(r);  <a,a>: r |] ==> P";
   32.35 +val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
   32.36  by (rtac wf_asym 1);
   32.37  by (REPEAT (resolve_tac prems 1));
   32.38  qed "wf_anti_refl";
   32.39 @@ -68,12 +68,12 @@
   32.40  (*This rewrite rule works upon formulae; thus it requires explicit use of
   32.41    H_cong to expose the equality*)
   32.42  goalw WF.thy [cut_def]
   32.43 -    "(cut f r x = cut g r x) = (!y. <y,x>:r --> f(y)=g(y))";
   32.44 +    "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
   32.45  by(simp_tac (HOL_ss addsimps [expand_fun_eq]
   32.46                      setloop (split_tac [expand_if])) 1);
   32.47  qed "cut_cut_eq";
   32.48  
   32.49 -goalw WF.thy [cut_def] "!!x. <x,a>:r ==> (cut f r a)(x) = f(x)";
   32.50 +goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
   32.51  by(asm_simp_tac HOL_ss 1);
   32.52  qed "cut_apply";
   32.53  
   32.54 @@ -81,12 +81,12 @@
   32.55  (*** is_recfun ***)
   32.56  
   32.57  goalw WF.thy [is_recfun_def,cut_def]
   32.58 -    "!!f. [| is_recfun r a H f;  ~<b,a>:r |] ==> f(b) = (@z.True)";
   32.59 +    "!!f. [| is_recfun r a H f;  ~(b,a):r |] ==> f(b) = (@z.True)";
   32.60  by (etac ssubst 1);
   32.61  by(asm_simp_tac HOL_ss 1);
   32.62  qed "is_recfun_undef";
   32.63  
   32.64 -(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   32.65 +(*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE
   32.66    mp amd allE  instantiate induction hypotheses*)
   32.67  fun indhyp_tac hyps =
   32.68      ares_tac (TrueI::hyps) ORELSE' 
   32.69 @@ -104,7 +104,7 @@
   32.70  
   32.71  val prems = goalw WF.thy [is_recfun_def,cut_def]
   32.72      "[| wf(r);  trans(r);  is_recfun r a H f;  is_recfun r b H g |] ==> \
   32.73 -    \ <x,a>:r --> <x,b>:r --> f(x)=g(x)";
   32.74 +    \ (x,a):r --> (x,b):r --> f(x)=g(x)";
   32.75  by (cut_facts_tac prems 1);
   32.76  by (etac wf_induct 1);
   32.77  by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
   32.78 @@ -115,7 +115,7 @@
   32.79  
   32.80  val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]
   32.81      "[| wf(r);  trans(r); \
   32.82 -\       is_recfun r a H f;  is_recfun r b H g;  <b,a>:r |] ==> \
   32.83 +\       is_recfun r a H f;  is_recfun r b H g;  (b,a):r |] ==> \
   32.84  \    cut f r b = g";
   32.85  val gundef = recgb RS is_recfun_undef
   32.86  and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
   32.87 @@ -150,13 +150,13 @@
   32.88  
   32.89  (*Beware incompleteness of unification!*)
   32.90  val prems = goal WF.thy
   32.91 -    "[| wf(r);  trans(r);  <c,a>:r;  <c,b>:r |] \
   32.92 +    "[| wf(r);  trans(r);  (c,a):r;  (c,b):r |] \
   32.93  \    ==> the_recfun r a H c = the_recfun r b H c";
   32.94  by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1));
   32.95  qed "the_recfun_equal";
   32.96  
   32.97  val prems = goal WF.thy
   32.98 -    "[| wf(r); trans(r); <b,a>:r |] \
   32.99 +    "[| wf(r); trans(r); (b,a):r |] \
  32.100  \    ==> cut (the_recfun r a H) r b = the_recfun r b H";
  32.101  by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1));
  32.102  qed "the_recfun_cut";
    33.1 --- a/src/HOL/WF.thy	Thu Mar 23 15:39:13 1995 +0100
    33.2 +++ b/src/HOL/WF.thy	Fri Mar 24 12:30:35 1995 +0100
    33.3 @@ -15,9 +15,9 @@
    33.4     the_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
    33.5  
    33.6  defs
    33.7 -  wf_def  "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
    33.8 +  wf_def  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
    33.9    
   33.10 -  cut_def 	 "cut f r x == (%y. if <y,x>:r then f y else @z.True)"
   33.11 +  cut_def 	 "cut f r x == (%y. if (y,x):r then f y else @z.True)"
   33.12  
   33.13    is_recfun_def  "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
   33.14  
    34.1 --- a/src/HOL/ex/Acc.ML	Thu Mar 23 15:39:13 1995 +0100
    34.2 +++ b/src/HOL/ex/Acc.ML	Fri Mar 24 12:30:35 1995 +0100
    34.3 @@ -13,12 +13,12 @@
    34.4  
    34.5  (*The intended introduction rule*)
    34.6  val prems = goal Acc.thy
    34.7 -    "[| !!b. <b,a>:r ==> b: acc(r) |] ==> a: acc(r)";
    34.8 +    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
    34.9  by (fast_tac (set_cs addIs (prems @ 
   34.10  			    map (rewrite_rule [pred_def]) acc.intrs)) 1);
   34.11  qed "accI";
   34.12  
   34.13 -goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
   34.14 +goal Acc.thy "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
   34.15  by (etac acc.elim 1);
   34.16  by (rewtac pred_def);
   34.17  by (fast_tac set_cs 1);
   34.18 @@ -26,7 +26,7 @@
   34.19  
   34.20  val [major,indhyp] = goal Acc.thy
   34.21      "[| a : acc(r);						\
   34.22 -\       !!x. [| x: acc(r);  ALL y. <y,x>:r --> P(y) |] ==> P(x)	\
   34.23 +\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x)	\
   34.24  \    |] ==> P(a)";
   34.25  by (rtac (major RS acc.induct) 1);
   34.26  by (rtac indhyp 1);
   34.27 @@ -44,7 +44,7 @@
   34.28  by (fast_tac set_cs 1);
   34.29  qed "acc_wfI";
   34.30  
   34.31 -val [major] = goal Acc.thy "wf(r) ==> ALL x. <x,y>: r | <y,x>:r --> y: acc(r)";
   34.32 +val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
   34.33  by (rtac (major RS wf_induct) 1);
   34.34  br (impI RS allI) 1;
   34.35  br accI 1;
    35.1 --- a/src/HOL/ex/Acc.thy	Thu Mar 23 15:39:13 1995 +0100
    35.2 +++ b/src/HOL/ex/Acc.thy	Fri Mar 24 12:30:35 1995 +0100
    35.3 @@ -16,7 +16,7 @@
    35.4    acc  :: "('a * 'a)set => 'a set"		(*Accessible part*)
    35.5  
    35.6  defs
    35.7 -  pred_def     "pred x r == {y. <y,x>:r}"
    35.8 +  pred_def     "pred x r == {y. (y,x):r}"
    35.9  
   35.10  inductive "acc(r)"
   35.11    intrs
    36.1 --- a/src/HOL/ex/LList.ML	Thu Mar 23 15:39:13 1995 +0100
    36.2 +++ b/src/HOL/ex/LList.ML	Fri Mar 24 12:30:35 1995 +0100
    36.3 @@ -135,7 +135,7 @@
    36.4  
    36.5  (*Lemma for the proof of llist_corec*)
    36.6  goal LList.thy
    36.7 -   "LList_corec a (%z.sum_case Inl (split(%v w.Inr(<Leaf(v),w>))) (f z)) : \
    36.8 +   "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
    36.9  \   llist(range(Leaf))";
   36.10  by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
   36.11  by (rtac rangeI 1);
   36.12 @@ -156,7 +156,7 @@
   36.13  end;
   36.14  qed "LListD_unfold";
   36.15  
   36.16 -goal LList.thy "!M N. <M,N> : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
   36.17 +goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
   36.18  by (res_inst_tac [("n", "k")] less_induct 1);
   36.19  by (safe_tac set_cs);
   36.20  by (etac LListD.elim 1);
   36.21 @@ -202,12 +202,12 @@
   36.22  ba 1;
   36.23  qed "LListD_coinduct";
   36.24  
   36.25 -goalw LList.thy [LListD_Fun_def,NIL_def] "<NIL,NIL> : LListD_Fun r s";
   36.26 +goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
   36.27  by (fast_tac set_cs 1);
   36.28  qed "LListD_Fun_NIL_I";
   36.29  
   36.30  goalw LList.thy [LListD_Fun_def,CONS_def]
   36.31 - "!!x. [| x:A;  <M,N>:s |] ==> <CONS x M, CONS x N> : LListD_Fun (diag A) s";
   36.32 + "!!x. [| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
   36.33  by (fast_tac univ_cs 1);
   36.34  qed "LListD_Fun_CONS_I";
   36.35  
   36.36 @@ -237,7 +237,7 @@
   36.37  qed "LListD_eq_diag";
   36.38  
   36.39  goal LList.thy 
   36.40 -    "!!M N. M: llist(A) ==> <M,M> : LListD_Fun (diag A) (X Un diag(llist(A)))";
   36.41 +    "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
   36.42  by (rtac (LListD_eq_diag RS subst) 1);
   36.43  br LListD_Fun_LListD_I 1;
   36.44  by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag, diagI]) 1);
   36.45 @@ -248,7 +248,7 @@
   36.46        [also admits true equality]
   36.47     Replace "A" by some particular set, like {x.True}??? *)
   36.48  goal LList.thy 
   36.49 -    "!!r. [| <M,N> : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
   36.50 +    "!!r. [| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
   36.51  \         |] ==>  M=N";
   36.52  by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
   36.53  by (etac LListD_coinduct 1);
   36.54 @@ -267,7 +267,7 @@
   36.55  by (rtac ext 1);
   36.56  (*next step avoids an unknown (and flexflex pair) in simplification*)
   36.57  by (res_inst_tac [("A", "{u.True}"),
   36.58 -		  ("r", "range(%u. <h1(u),h2(u)>)")] LList_equalityI 1);
   36.59 +		  ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
   36.60  by (rtac rangeI 1);
   36.61  by (safe_tac set_cs);
   36.62  by (stac prem1 1);
   36.63 @@ -332,14 +332,14 @@
   36.64  by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
   36.65  qed "Lconst_type";
   36.66  
   36.67 -goal LList.thy "Lconst(M) = LList_corec M (%x.Inr(<x,x>))";
   36.68 +goal LList.thy "Lconst(M) = LList_corec M (%x.Inr((x,x)))";
   36.69  by (rtac (equals_LList_corec RS fun_cong) 1);
   36.70  by (simp_tac sum_ss 1);
   36.71  by (rtac Lconst 1);
   36.72  qed "Lconst_eq_LList_corec";
   36.73  
   36.74  (*Thus we could have used gfp in the definition of Lconst*)
   36.75 -goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr(<x,x>))";
   36.76 +goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))";
   36.77  by (rtac (equals_LList_corec RS fun_cong) 1);
   36.78  by (simp_tac sum_ss 1);
   36.79  by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
   36.80 @@ -420,8 +420,8 @@
   36.81   "[| M: llist(A); g(NIL): llist(A); 				\
   36.82  \    f(NIL)=g(NIL);						\
   36.83  \    !!x l. [| x:A;  l: llist(A) |] ==>				\
   36.84 -\	    <f(CONS x l),g(CONS x l)> :				\
   36.85 -\               LListD_Fun (diag A) ((%u.<f(u),g(u)>)``llist(A) Un  \
   36.86 +\	    (f(CONS x l),g(CONS x l)) :				\
   36.87 +\               LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un  \
   36.88  \                                   diag(llist(A)))		\
   36.89  \ |] ==> f(M) = g(M)";
   36.90  by (rtac LList_equalityI 1);
   36.91 @@ -637,7 +637,7 @@
   36.92  qed "prod_fun_lemma";
   36.93  
   36.94  goal LList.thy
   36.95 -    "prod_fun Rep_llist  Rep_llist `` range(%x. <x, x>) = \
   36.96 +    "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
   36.97  \    diag(llist(range(Leaf)))";
   36.98  br equalityI 1;
   36.99  by (fast_tac (univ_cs addIs [Rep_llist]) 1);
  36.100 @@ -647,7 +647,7 @@
  36.101  (** To show two llists are equal, exhibit a bisimulation! 
  36.102        [also admits true equality] **)
  36.103  val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
  36.104 -    "[| <l1,l2> : r;  r <= llistD_Fun(r Un range(%x.<x,x>)) |] ==> l1=l2";
  36.105 +    "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
  36.106  by (rtac (inj_Rep_llist RS injD) 1);
  36.107  by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
  36.108  		  ("A", "range(Leaf)")] 
  36.109 @@ -664,19 +664,19 @@
  36.110  qed "llist_equalityI";
  36.111  
  36.112  (** Rules to prove the 2nd premise of llist_equalityI **)
  36.113 -goalw LList.thy [llistD_Fun_def,LNil_def] "<LNil,LNil> : llistD_Fun(r)";
  36.114 +goalw LList.thy [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
  36.115  by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
  36.116  qed "llistD_Fun_LNil_I";
  36.117  
  36.118  val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def]
  36.119 -    "<l1,l2>:r ==> <LCons x l1, LCons x l2> : llistD_Fun(r)";
  36.120 +    "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
  36.121  by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
  36.122  by (rtac (prem RS prod_fun_imageI) 1);
  36.123  qed "llistD_Fun_LCons_I";
  36.124  
  36.125  (*Utilise the "strong" part, i.e. gfp(f)*)
  36.126  goalw LList.thy [llistD_Fun_def]
  36.127 -     "!!l. <l,l> : llistD_Fun(r Un range(%x.<x,x>))";
  36.128 +     "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
  36.129  br (Rep_llist_inverse RS subst) 1;
  36.130  br prod_fun_imageI 1;
  36.131  by (rtac (image_Un RS ssubst) 1);
  36.132 @@ -687,10 +687,10 @@
  36.133  (*A special case of list_equality for functions over lazy lists*)
  36.134  val [prem1,prem2] = goal LList.thy
  36.135      "[| f(LNil)=g(LNil);						\
  36.136 -\       !!x l. <f(LCons x l),g(LCons x l)> :				\
  36.137 -\              llistD_Fun(range(%u. <f(u),g(u)>) Un range(%v. <v,v>))	\
  36.138 +\       !!x l. (f(LCons x l),g(LCons x l)) :				\
  36.139 +\              llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))	\
  36.140  \    |]	==> f(l) = (g(l :: 'a llist) :: 'b llist)";
  36.141 -by (res_inst_tac [("r", "range(%u. <f(u),g(u)>)")] llist_equalityI 1);
  36.142 +by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
  36.143  by (rtac rangeI 1);
  36.144  by (rtac subsetI 1);
  36.145  by (etac rangeE 1);
  36.146 @@ -744,7 +744,7 @@
  36.147  qed "iterates";
  36.148  
  36.149  goal LList.thy "lmap f (iterates f x) = iterates f (f x)";
  36.150 -by (res_inst_tac [("r", "range(%u.<lmap f (iterates f u),iterates f (f u)>)")] 
  36.151 +by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
  36.152      llist_equalityI 1);
  36.153  by (rtac rangeI 1);
  36.154  by (safe_tac set_cs);
  36.155 @@ -777,14 +777,14 @@
  36.156  val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
  36.157   [("f","Pair")] (standard(refl RS cong RS cong));
  36.158  
  36.159 -(*The bisimulation consists of {<lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u))>}
  36.160 +(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
  36.161    for all u and all n::nat.*)
  36.162  val [prem] = goal LList.thy
  36.163      "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
  36.164  br ext 1;
  36.165  by (res_inst_tac [("r", 
  36.166 -   "UN u. range(%n. <nat_rec n (h u) (%m y.lmap f y), \
  36.167 -\                    nat_rec n (iterates f u) (%m y.lmap f y)>)")] 
  36.168 +   "UN u. range(%n. (nat_rec n (h u) (%m y.lmap f y), \
  36.169 +\                    nat_rec n (iterates f u) (%m y.lmap f y)))")] 
  36.170      llist_equalityI 1);
  36.171  by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
  36.172  by (safe_tac set_cs);
  36.173 @@ -834,7 +834,7 @@
  36.174  
  36.175  (*The infinite first argument blocks the second*)
  36.176  goal LList.thy "lappend (iterates f x) N = iterates f x";
  36.177 -by (res_inst_tac [("r", "range(%u.<lappend (iterates f u) N,iterates f u>)")] 
  36.178 +by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
  36.179      llist_equalityI 1);
  36.180  by (rtac rangeI 1);
  36.181  by (safe_tac set_cs);
  36.182 @@ -848,7 +848,7 @@
  36.183  goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
  36.184  by (res_inst_tac 
  36.185      [("r",  
  36.186 -      "UN n. range(%l.<lmap f (lappend l n),lappend (lmap f l) (lmap f n)>)")] 
  36.187 +      "UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")] 
  36.188      llist_equalityI 1);
  36.189  by (rtac UN1_I 1);
  36.190  by (rtac rangeI 1);
    37.1 --- a/src/HOL/ex/LList.thy	Thu Mar 23 15:39:13 1995 +0100
    37.2 +++ b/src/HOL/ex/LList.thy	Fri Mar 24 12:30:35 1995 +0100
    37.3 @@ -19,8 +19,8 @@
    37.4  Previous definition of llistD_Fun was explicit:
    37.5    llistD_Fun_def
    37.6     "llistD_Fun(r) == 	\
    37.7 -\       {<LNil,LNil>}  Un  	\
    37.8 -\       (UN x. (split(%l1 l2.<LCons(x,l1),LCons(x,l2)>))``r)"
    37.9 +\       {(LNil,LNil)}  Un  	\
   37.10 +\       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
   37.11  *)
   37.12  
   37.13  LList = Gfp + SList +
   37.14 @@ -69,9 +69,9 @@
   37.15  
   37.16  coinductive "LListD(r)"
   37.17    intrs
   37.18 -    NIL_I  "<NIL, NIL> : LListD(r)"
   37.19 -    CONS_I "[| <a,b>: r;  <M,N> : LListD(r)   \
   37.20 -\	    |] ==> <CONS a M, CONS b N> : LListD(r)"
   37.21 +    NIL_I  "(NIL, NIL) : LListD(r)"
   37.22 +    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   \
   37.23 +\	    |] ==> (CONS a M, CONS b N) : LListD(r)"
   37.24  
   37.25  defs
   37.26    (*Now used exclusively for abbreviating the coinduction rule*)
   37.27 @@ -79,9 +79,9 @@
   37.28  \		  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   37.29  
   37.30    LListD_Fun_def "LListD_Fun r X ==   \
   37.31 -\		  {z. z = <NIL, NIL> |   \
   37.32 -\		      (? M N a b. z = <CONS a M, CONS b N> &   \
   37.33 -\		                  <a, b> : r & <M, N> : X)}"
   37.34 +\		  {z. z = (NIL, NIL) |   \
   37.35 +\		      (? M N a b. z = (CONS a M, CONS b N) &   \
   37.36 +\		                  (a, b) : r & (M, N) : X)}"
   37.37  
   37.38    (*defining the abstract constructors*)
   37.39    LNil_def  	"LNil == Abs_llist(NIL)"
   37.40 @@ -102,7 +102,7 @@
   37.41    llist_corec_def
   37.42     "llist_corec a f == \
   37.43  \       Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \
   37.44 -\                                    (split(%v w. Inr(<Leaf(v), w>))) (f z)))"
   37.45 +\                                    (split(%v w. Inr((Leaf(v), w)))) (f z)))"
   37.46  
   37.47    llistD_Fun_def
   37.48     "llistD_Fun(r) == 	\
   37.49 @@ -113,28 +113,28 @@
   37.50    Lconst_def	"Lconst(M) == lfp(%N. CONS M N)"     
   37.51  
   37.52    Lmap_def
   37.53 -   "Lmap f M == LList_corec M (List_case (Inl Unity) (%x M'. Inr(<f(x), M'>)))"
   37.54 +   "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
   37.55  
   37.56    lmap_def
   37.57 -   "lmap f l == llist_corec l (llist_case (Inl Unity) (%y z. Inr(<f(y), z>)))"
   37.58 +   "lmap f l == llist_corec l (llist_case (Inl ()) (%y z. Inr((f(y), z))))"
   37.59  
   37.60 -  iterates_def	"iterates f a == llist_corec a (%x. Inr(<x, f(x)>))"     
   37.61 +  iterates_def	"iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
   37.62  
   37.63  (*Append generates its result by applying f, where
   37.64 -    f(<NIL,NIL>) = Inl(Unity)
   37.65 -    f(<NIL, CONS N1 N2>) = Inr(<N1, <NIL,N2>)
   37.66 -    f(<CONS M1 M2, N>)    = Inr(<M1, <M2,N>)
   37.67 +    f((NIL,NIL)) = Inl(())
   37.68 +    f((NIL, CONS N1 N2)) = Inr((N1, (NIL,N2))
   37.69 +    f((CONS M1 M2, N))    = Inr((M1, (M2,N))
   37.70  *)
   37.71  
   37.72    Lappend_def
   37.73 -   "Lappend M N == LList_corec <M,N>	   				     \
   37.74 -\     (split(List_case (List_case (Inl Unity) (%N1 N2. Inr(<N1, <NIL,N2>>))) \
   37.75 -\                      (%M1 M2 N. Inr(<M1, <M2,N>>))))"
   37.76 +   "Lappend M N == LList_corec (M,N)	   				     \
   37.77 +\     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) \
   37.78 +\                      (%M1 M2 N. Inr((M1, (M2,N))))))"
   37.79  
   37.80    lappend_def
   37.81 -   "lappend l n == llist_corec <l,n>	   				     \
   37.82 -\   (split(llist_case (llist_case (Inl Unity) (%n1 n2. Inr(<n1, <LNil,n2>>))) \
   37.83 -\                     (%l1 l2 n. Inr(<l1, <l2,n>>))))"
   37.84 +   "lappend l n == llist_corec (l,n)	   				     \
   37.85 +\   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) \
   37.86 +\                     (%l1 l2 n. Inr((l1, (l2,n))))))"
   37.87  
   37.88  rules
   37.89      (*faking a type definition...*)
    38.1 --- a/src/HOL/ex/LexProd.ML	Thu Mar 23 15:39:13 1995 +0100
    38.2 +++ b/src/HOL/ex/LexProd.ML	Fri Mar 24 12:30:35 1995 +0100
    38.3 @@ -7,7 +7,7 @@
    38.4  The lexicographic product of two wellfounded relations is again wellfounded.
    38.5  *)
    38.6  
    38.7 -val prems = goal Prod.thy "!a b. P(<a,b>) ==> !p.P(p)";
    38.8 +val prems = goal Prod.thy "!a b. P((a,b)) ==> !p.P(p)";
    38.9  by (cut_facts_tac prems 1);
   38.10  by (rtac allI 1);
   38.11  by (rtac (surjective_pairing RS ssubst) 1);
    39.1 --- a/src/HOL/ex/LexProd.thy	Thu Mar 23 15:39:13 1995 +0100
    39.2 +++ b/src/HOL/ex/LexProd.thy	Fri Mar 24 12:30:35 1995 +0100
    39.3 @@ -10,6 +10,6 @@
    39.4  consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
    39.5  rules
    39.6  lex_prod_def "ra**rb == {p. ? a a' b b'. \
    39.7 -\	p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb)}"
    39.8 +\	p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
    39.9  end
   39.10  
    40.1 --- a/src/HOL/ex/MT.ML	Thu Mar 23 15:39:13 1995 +0100
    40.2 +++ b/src/HOL/ex/MT.ML	Fri Mar 24 12:30:35 1995 +0100
    40.3 @@ -45,13 +45,13 @@
    40.4        (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
    40.5      );
    40.6  
    40.7 -val prems = goal MT.thy "P a b ==> P (fst <a,b>) (snd <a,b>)";
    40.8 +val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
    40.9  by (rtac (fst_conv RS ssubst) 1);
   40.10  by (rtac (snd_conv RS ssubst) 1);
   40.11  by (resolve_tac prems 1);
   40.12  qed "infsys_p1";
   40.13  
   40.14 -val prems = goal MT.thy "P (fst <a,b>) (snd <a,b>) ==> P a b";
   40.15 +val prems = goal MT.thy "P (fst (a,b)) (snd (a,b)) ==> P a b";
   40.16  by (cut_facts_tac prems 1);
   40.17  by (dtac (fst_conv RS subst) 1);
   40.18  by (dtac (snd_conv RS subst) 1);
   40.19 @@ -59,7 +59,7 @@
   40.20  qed "infsys_p2";
   40.21  
   40.22  val prems = goal MT.thy 
   40.23 -  "P a b c ==> P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>)";
   40.24 +  "P a b c ==> P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
   40.25  by (rtac (fst_conv RS ssubst) 1);
   40.26  by (rtac (fst_conv RS ssubst) 1);
   40.27  by (rtac (snd_conv RS ssubst) 1);
   40.28 @@ -68,7 +68,7 @@
   40.29  qed "infsys_pp1";
   40.30  
   40.31  val prems = goal MT.thy 
   40.32 -  "P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>) ==> P a b c";
   40.33 +  "P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c)) ==> P a b c";
   40.34  by (cut_facts_tac prems 1);
   40.35  by (dtac (fst_conv RS subst) 1);
   40.36  by (dtac (fst_conv RS subst) 1);
   40.37 @@ -240,23 +240,23 @@
   40.38  
   40.39  val prems = goalw MT.thy [eval_def, eval_rel_def]
   40.40    " [| ve |- e ---> v; \
   40.41 -\      !!ve c. P(<<ve,e_const(c)>,v_const(c)>); \
   40.42 -\      !!ev ve. ev:ve_dom(ve) ==> P(<<ve,e_var(ev)>,ve_app ve ev>); \
   40.43 -\      !!ev ve e. P(<<ve,fn ev => e>,v_clos(<|ev,e,ve|>)>); \
   40.44 +\      !!ve c. P(((ve,e_const(c)),v_const(c))); \
   40.45 +\      !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
   40.46 +\      !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
   40.47  \      !!ev1 ev2 ve cl e. \
   40.48  \        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
   40.49 -\        P(<<ve,fix ev2(ev1) = e>,v_clos(cl)>); \
   40.50 +\        P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
   40.51  \      !!ve c1 c2 e1 e2. \
   40.52 -\        [| P(<<ve,e1>,v_const(c1)>); P(<<ve,e2>,v_const(c2)>) |] ==> \
   40.53 -\        P(<<ve,e1 @ e2>,v_const(c_app c1 c2)>); \
   40.54 +\        [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
   40.55 +\        P(((ve,e1 @ e2),v_const(c_app c1 c2))); \
   40.56  \      !!ve vem xm e1 e2 em v v2. \
   40.57 -\        [|  P(<<ve,e1>,v_clos(<|xm,em,vem|>)>); \
   40.58 -\            P(<<ve,e2>,v2>); \
   40.59 -\            P(<<vem + {xm |-> v2},em>,v>) \
   40.60 +\        [|  P(((ve,e1),v_clos(<|xm,em,vem|>))); \
   40.61 +\            P(((ve,e2),v2)); \
   40.62 +\            P(((vem + {xm |-> v2},em),v)) \
   40.63  \        |] ==> \
   40.64 -\        P(<<ve,e1 @ e2>,v>) \
   40.65 +\        P(((ve,e1 @ e2),v)) \
   40.66  \   |] ==> \
   40.67 -\   P(<<ve,e>,v>)";
   40.68 +\   P(((ve,e),v))";
   40.69  by (resolve_tac (prems RL [lfp_ind2]) 1);
   40.70  by (rtac eval_fun_mono 1);
   40.71  by (rewtac eval_fun_def);
   40.72 @@ -356,23 +356,23 @@
   40.73  
   40.74  val prems = goalw MT.thy [elab_def, elab_rel_def]
   40.75    " [| te |- e ===> t; \
   40.76 -\      !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
   40.77 -\      !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \
   40.78 +\      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
   40.79 +\      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
   40.80  \      !!te x e t1 t2. \
   40.81 -\        [| te + {x |=> t1} |- e ===> t2; P(<<te + {x |=> t1},e>,t2>) |] ==> \
   40.82 -\        P(<<te,fn x => e>,t1->t2>); \
   40.83 +\        [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
   40.84 +\        P(((te,fn x => e),t1->t2)); \
   40.85  \      !!te f x e t1 t2. \
   40.86  \        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
   40.87 -\           P(<<te + {f |=> t1->t2} + {x |=> t1},e>,t2>) \
   40.88 +\           P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
   40.89  \        |] ==> \
   40.90 -\        P(<<te,fix f(x) = e>,t1->t2>); \
   40.91 +\        P(((te,fix f(x) = e),t1->t2)); \
   40.92  \      !!te e1 e2 t1 t2. \
   40.93 -\        [| te |- e1 ===> t1->t2; P(<<te,e1>,t1->t2>); \
   40.94 -\           te |- e2 ===> t1; P(<<te,e2>,t1>) \
   40.95 +\        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
   40.96 +\           te |- e2 ===> t1; P(((te,e2),t1)) \
   40.97  \        |] ==> \
   40.98 -\        P(<<te,e1 @ e2>,t2>) \
   40.99 +\        P(((te,e1 @ e2),t2)) \
  40.100  \   |] ==> \
  40.101 -\   P(<<te,e>,t>)";
  40.102 +\   P(((te,e),t))";
  40.103  by (resolve_tac (prems RL [lfp_ind2]) 1);
  40.104  by (rtac elab_fun_mono 1);
  40.105  by (rewtac elab_fun_def);
  40.106 @@ -412,18 +412,18 @@
  40.107  
  40.108  val prems = goalw MT.thy [elab_def, elab_rel_def]
  40.109    " [| te |- e ===> t; \
  40.110 -\      !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \
  40.111 -\      !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \
  40.112 +\      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
  40.113 +\      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
  40.114  \      !!te x e t1 t2. \
  40.115 -\        te + {x |=> t1} |- e ===> t2 ==> P(<<te,fn x => e>,t1->t2>); \
  40.116 +\        te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
  40.117  \      !!te f x e t1 t2. \
  40.118  \        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
  40.119 -\        P(<<te,fix f(x) = e>,t1->t2>); \
  40.120 +\        P(((te,fix f(x) = e),t1->t2)); \
  40.121  \      !!te e1 e2 t1 t2. \
  40.122  \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
  40.123 -\        P(<<te,e1 @ e2>,t2>) \
  40.124 +\        P(((te,e1 @ e2),t2)) \
  40.125  \   |] ==> \
  40.126 -\   P(<<te,e>,t>)";
  40.127 +\   P(((te,e),t))";
  40.128  by (resolve_tac (prems RL [lfp_elim2]) 1);
  40.129  by (rtac elab_fun_mono 1);
  40.130  by (rewtac elab_fun_def);
  40.131 @@ -545,7 +545,7 @@
  40.132  
  40.133  (* First strong indtroduction (co-induction) rule for hasty_rel *)
  40.134  
  40.135 -val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> <v_const(c),t> : hasty_rel";
  40.136 +val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
  40.137  by (cut_facts_tac prems 1);
  40.138  by (rtac gfp_coind2 1);
  40.139  by (rewtac MT.hasty_fun_def);
  40.140 @@ -561,9 +561,9 @@
  40.141  \       ve_dom(ve) = te_dom(te); \
  40.142  \       ! ev1. \
  40.143  \         ev1:ve_dom(ve) --> \
  40.144 -\         <ve_app ve ev1,te_app te ev1> : {<v_clos(<|ev,e,ve|>),t>} Un hasty_rel \
  40.145 +\         (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
  40.146  \   |] ==> \
  40.147 -\   <v_clos(<|ev,e,ve|>),t> : hasty_rel";
  40.148 +\   (v_clos(<|ev,e,ve|>),t) : hasty_rel";
  40.149  by (cut_facts_tac prems 1);
  40.150  by (rtac gfp_coind2 1);
  40.151  by (rewtac hasty_fun_def);
  40.152 @@ -575,14 +575,14 @@
  40.153  (* Elimination rule for hasty_rel *)
  40.154  
  40.155  val prems = goalw MT.thy [hasty_rel_def]
  40.156 -  " [| !! c t.c isof t ==> P(<v_const(c),t>); \
  40.157 +  " [| !! c t.c isof t ==> P((v_const(c),t)); \
  40.158  \      !! te ev e t ve. \
  40.159  \        [| te |- fn ev => e ===> t; \
  40.160  \           ve_dom(ve) = te_dom(te); \
  40.161 -\           !ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
  40.162 -\        |] ==> P(<v_clos(<|ev,e,ve|>),t>); \
  40.163 -\      <v,t> : hasty_rel \
  40.164 -\   |] ==> P(<v,t>)";
  40.165 +\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
  40.166 +\        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
  40.167 +\      (v,t) : hasty_rel \
  40.168 +\   |] ==> P((v,t))";
  40.169  by (cut_facts_tac prems 1);
  40.170  by (etac gfp_elim2 1);
  40.171  by (rtac mono_hasty_fun 1);
  40.172 @@ -595,12 +595,12 @@
  40.173  qed "hasty_rel_elim0";
  40.174  
  40.175  val prems = goal MT.thy 
  40.176 -  " [| <v,t> : hasty_rel; \
  40.177 +  " [| (v,t) : hasty_rel; \
  40.178  \      !! c t.c isof t ==> P (v_const c) t; \
  40.179  \      !! te ev e t ve. \
  40.180  \        [| te |- fn ev => e ===> t; \
  40.181  \           ve_dom(ve) = te_dom(te); \
  40.182 -\           !ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
  40.183 +\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
  40.184  \        |] ==> P (v_clos <|ev,e,ve|>) t \
  40.185  \   |] ==> P v t";
  40.186  by (res_inst_tac [("P","P")] infsys_p2 1);
    41.1 --- a/src/HOL/ex/MT.thy	Thu Mar 23 15:39:13 1995 +0100
    41.2 +++ b/src/HOL/ex/MT.thy	Fri Mar 24 12:30:35 1995 +0100
    41.3 @@ -196,27 +196,27 @@
    41.4    eval_fun_def 
    41.5      " eval_fun(s) == \
    41.6  \     { pp. \
    41.7 -\       (? ve c. pp=<<ve,e_const(c)>,v_const(c)>) | \
    41.8 -\       (? ve x. pp=<<ve,e_var(x)>,ve_app ve x> & x:ve_dom(ve)) |\
    41.9 -\       (? ve e x. pp=<<ve,fn x => e>,v_clos(<|x,e,ve|>)>)| \
   41.10 +\       (? ve c. pp=((ve,e_const(c)),v_const(c))) | \
   41.11 +\       (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |\
   41.12 +\       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| \
   41.13  \       ( ? ve e x f cl. \
   41.14 -\           pp=<<ve,fix f(x) = e>,v_clos(cl)> & \
   41.15 +\           pp=((ve,fix f(x) = e),v_clos(cl)) & \
   41.16  \           cl=<|x, e, ve+{f |-> v_clos(cl)} |>  \
   41.17  \       ) | \
   41.18  \       ( ? ve e1 e2 c1 c2. \
   41.19 -\           pp=<<ve,e1 @ e2>,v_const(c_app c1 c2)> & \
   41.20 -\           <<ve,e1>,v_const(c1)>:s & <<ve,e2>,v_const(c2)>:s \
   41.21 +\           pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & \
   41.22 +\           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s \
   41.23  \       ) | \
   41.24  \       ( ? ve vem e1 e2 em xm v v2. \
   41.25 -\           pp=<<ve,e1 @ e2>,v> & \
   41.26 -\           <<ve,e1>,v_clos(<|xm,em,vem|>)>:s & \
   41.27 -\           <<ve,e2>,v2>:s & \
   41.28 -\           <<vem+{xm |-> v2},em>,v>:s \
   41.29 +\           pp=((ve,e1 @ e2),v) & \
   41.30 +\           ((ve,e1),v_clos(<|xm,em,vem|>)):s & \
   41.31 +\           ((ve,e2),v2):s & \
   41.32 +\           ((vem+{xm |-> v2},em),v):s \
   41.33  \       ) \
   41.34  \     }"
   41.35  
   41.36    eval_rel_def "eval_rel == lfp(eval_fun)"
   41.37 -  eval_def "ve |- e ---> v == <<ve,e>,v>:eval_rel"
   41.38 +  eval_def "ve |- e ---> v == ((ve,e),v):eval_rel"
   41.39  
   41.40  (* The static semantics is defined in the same way as the dynamic
   41.41  semantics.  The relation te |- e ===> t express the expression e has the
   41.42 @@ -226,19 +226,19 @@
   41.43    elab_fun_def 
   41.44    "elab_fun(s) == \
   41.45  \  { pp. \
   41.46 -\    (? te c t. pp=<<te,e_const(c)>,t> & c isof t) | \
   41.47 -\    (? te x. pp=<<te,e_var(x)>,te_app te x> & x:te_dom(te)) | \
   41.48 -\    (? te x e t1 t2. pp=<<te,fn x => e>,t1->t2> & <<te+{x |=> t1},e>,t2>:s) | \
   41.49 +\    (? te c t. pp=((te,e_const(c)),t) & c isof t) | \
   41.50 +\    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | \
   41.51 +\    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | \
   41.52  \    (? te f x e t1 t2. \
   41.53 -\       pp=<<te,fix f(x)=e>,t1->t2> & <<te+{f |=> t1->t2}+{x |=> t1},e>,t2>:s \
   41.54 +\       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s \
   41.55  \    ) | \
   41.56  \    (? te e1 e2 t1 t2. \
   41.57 -\       pp=<<te,e1 @ e2>,t2> & <<te,e1>,t1->t2>:s & <<te,e2>,t1>:s \
   41.58 +\       pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s \
   41.59  \    ) \
   41.60  \  }"
   41.61  
   41.62    elab_rel_def "elab_rel == lfp(elab_fun)"
   41.63 -  elab_def "te |- e ===> t == <<te,e>,t>:elab_rel"
   41.64 +  elab_def "te |- e ===> t == ((te,e),t):elab_rel"
   41.65  
   41.66  (* The original correspondence relation *)
   41.67  
   41.68 @@ -258,18 +258,18 @@
   41.69    hasty_fun_def
   41.70      " hasty_fun(r) == \
   41.71  \     { p. \
   41.72 -\       ( ? c t. p = <v_const(c),t> & c isof t) | \
   41.73 +\       ( ? c t. p = (v_const(c),t) & c isof t) | \
   41.74  \       ( ? ev e ve t te. \
   41.75 -\           p = <v_clos(<|ev,e,ve|>),t> & \
   41.76 +\           p = (v_clos(<|ev,e,ve|>),t) & \
   41.77  \           te |- fn ev => e ===> t & \
   41.78  \           ve_dom(ve) = te_dom(te) & \
   41.79 -\           (! ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : r) \
   41.80 +\           (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) \
   41.81  \       ) \
   41.82  \     } \
   41.83  \   "
   41.84  
   41.85    hasty_rel_def "hasty_rel == gfp(hasty_fun)"
   41.86 -  hasty_def "v hasty t == <v,t> : hasty_rel"
   41.87 +  hasty_def "v hasty t == (v,t) : hasty_rel"
   41.88    hasty_env_def 
   41.89      " ve hastyenv te == \
   41.90  \     ve_dom(ve) = te_dom(te) & \
    42.1 --- a/src/HOL/ex/ROOT.ML	Thu Mar 23 15:39:13 1995 +0100
    42.2 +++ b/src/HOL/ex/ROOT.ML	Fri Mar 24 12:30:35 1995 +0100
    42.3 @@ -8,7 +8,7 @@
    42.4  
    42.5  CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
    42.6  
    42.7 -(writeln"Root file for CHOL examples";
    42.8 +(writeln "Root file for CHOL examples";
    42.9   proof_timing := true;
   42.10   loadpath := ["ex"];
   42.11   time_use     "ex/cla.ML";
   42.12 @@ -28,5 +28,5 @@
   42.13   time_use_thy "Term";
   42.14   time_use_thy "Simult";
   42.15   time_use_thy "MT";
   42.16 - writeln     "END: Root file for HOL examples"
   42.17 + writeln "END: Root file for CHOL examples"
   42.18  )  handle _ => exit 1;
    43.1 --- a/src/HOL/ex/SList.ML	Thu Mar 23 15:39:13 1995 +0100
    43.2 +++ b/src/HOL/ex/SList.ML	Fri Mar 24 12:30:35 1995 +0100
    43.3 @@ -156,18 +156,18 @@
    43.4  (** pred_sexp lemmas **)
    43.5  
    43.6  goalw SList.thy [CONS_def,In1_def]
    43.7 -    "!!M. [| M: sexp;  N: sexp |] ==> <M, CONS M N> : pred_sexp^+";
    43.8 +    "!!M. [| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
    43.9  by (asm_simp_tac pred_sexp_ss 1);
   43.10  qed "pred_sexp_CONS_I1";
   43.11  
   43.12  goalw SList.thy [CONS_def,In1_def]
   43.13 -    "!!M. [| M: sexp;  N: sexp |] ==> <N, CONS M N> : pred_sexp^+";
   43.14 +    "!!M. [| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
   43.15  by (asm_simp_tac pred_sexp_ss 1);
   43.16  qed "pred_sexp_CONS_I2";
   43.17  
   43.18  val [prem] = goal SList.thy
   43.19 -    "<CONS M1 M2, N> : pred_sexp^+ ==> \
   43.20 -\    <M1,N> : pred_sexp^+ & <M2,N> : pred_sexp^+";
   43.21 +    "(CONS M1 M2, N) : pred_sexp^+ ==> \
   43.22 +\    (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+";
   43.23  by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS 
   43.24  		   subsetD RS SigmaE2)) 1);
   43.25  by (etac (sexp_CONS_D RS conjE) 1);
    44.1 --- a/src/HOL/ex/Term.ML	Thu Mar 23 15:39:13 1995 +0100
    44.2 +++ b/src/HOL/ex/Term.ML	Fri Mar 24 12:30:35 1995 +0100
    44.3 @@ -119,7 +119,7 @@
    44.4  
    44.5  val [prem] = goal Term.thy
    44.6      "N: list(term(A)) ==>  \
    44.7 -\    !M. <N,M>: pred_sexp^+ --> \
    44.8 +\    !M. (N,M): pred_sexp^+ --> \
    44.9  \        Abs_map (cut h (pred_sexp^+) M) N = \
   44.10  \        Abs_map h N";
   44.11  by (rtac (prem RS list.induct) 1);
    45.1 --- a/src/HOL/ex/rel.ML	Thu Mar 23 15:39:13 1995 +0100
    45.2 +++ b/src/HOL/ex/rel.ML	Fri Mar 24 12:30:35 1995 +0100
    45.3 @@ -17,8 +17,8 @@
    45.4   ],
    45.5   None)
    45.6   [
    45.7 -  ("domain_def",     "domain(r) == {a. ? b. <a,b> : r}" ),
    45.8 -  ("range2_def",     "range2(r) == {b. ? a. <a,b> : r}" ),
    45.9 +  ("domain_def",     "domain(r) == {a. ? b. (a,b) : r}" ),
   45.10 +  ("range2_def",     "range2(r) == {b. ? a. (a,b) : r}" ),
   45.11    ("field_def",      "field(r)  == domain(r) Un range2(r)" )
   45.12   ];
   45.13  end;
   45.14 @@ -33,12 +33,12 @@
   45.15  
   45.16  (*** domain ***)
   45.17  
   45.18 -val [prem] = goalw Rel.thy [domain_def,Pair_def] "<a,b>: r ==> a : domain(r)";
   45.19 +val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)";
   45.20  by (fast_tac (set_cs addIs [prem]) 1);
   45.21  qed "domainI";
   45.22  
   45.23  val major::prems = goalw Rel.thy [domain_def]
   45.24 -    "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P";
   45.25 +    "[| a : domain(r);  !!y. (a,y): r ==> P |] ==> P";
   45.26  by (rtac (major RS CollectE) 1);
   45.27  by (etac exE 1);
   45.28  by (REPEAT (ares_tac prems 1));
   45.29 @@ -47,12 +47,12 @@
   45.30  
   45.31  (*** range2 ***)
   45.32  
   45.33 -val [prem] = goalw Rel.thy [range2_def,Pair_def] "<a,b>: r ==> b : range2(r)";
   45.34 +val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)";
   45.35  by (fast_tac (set_cs addIs [prem]) 1);
   45.36  qed "range2I";
   45.37  
   45.38  val major::prems = goalw Rel.thy [range2_def]
   45.39 -    "[| b : range2(r);  !!x. <x,b>: r ==> P |] ==> P";
   45.40 +    "[| b : range2(r);  !!x. (x,b): r ==> P |] ==> P";
   45.41  by (rtac (major RS CollectE) 1);
   45.42  by (etac exE 1);
   45.43  by (REPEAT (ares_tac prems 1));
   45.44 @@ -61,16 +61,16 @@
   45.45  
   45.46  (*** field ***)
   45.47  
   45.48 -val [prem] = goalw Rel.thy [field_def] "<a,b>: r ==> a : field(r)";
   45.49 +val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> a : field(r)";
   45.50  by (rtac (prem RS domainI RS UnI1) 1);
   45.51  qed "fieldI1";
   45.52  
   45.53 -val [prem] = goalw Rel.thy [field_def] "<a,b>: r ==> b : field(r)";
   45.54 +val [prem] = goalw Rel.thy [field_def] "(a,b): r ==> b : field(r)";
   45.55  by (rtac (prem RS range2I RS UnI2) 1);
   45.56  qed "fieldI2";
   45.57  
   45.58  val [prem] = goalw Rel.thy [field_def]
   45.59 -    "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)";
   45.60 +    "(~ (c,a):r ==> (a,b): r) ==> a : field(r)";
   45.61  by (rtac (prem RS domainI RS UnCI) 1);
   45.62  by (swap_res_tac [range2I] 1);
   45.63  by (etac notnotD 1);
   45.64 @@ -78,8 +78,8 @@
   45.65  
   45.66  val major::prems = goalw Rel.thy [field_def]
   45.67       "[| a : field(r);  \
   45.68 -\        !!x. <a,x>: r ==> P;  \
   45.69 -\        !!x. <x,a>: r ==> P        |] ==> P";
   45.70 +\        !!x. (a,x): r ==> P;  \
   45.71 +\        !!x. (x,a): r ==> P        |] ==> P";
   45.72  by (rtac (major RS UnE) 1);
   45.73  by (REPEAT (eresolve_tac (prems@[domainE,range2E]) 1));
   45.74  qed "fieldE";
   45.75 @@ -98,7 +98,7 @@
   45.76  (*If r allows well-founded induction then wf(r)*)
   45.77  val [prem1,prem2] = goalw Rel.thy [wf_def] 
   45.78      "[| field(r)<=A;  \
   45.79 -\       !!P u. ! x:A. (! y. <y,x>: r --> P(y)) --> P(x) ==> P(u) |]  \
   45.80 +\       !!P u. ! x:A. (! y. (y,x): r --> P(y)) --> P(x) ==> P(u) |]  \
   45.81  \    ==>  wf(r)";
   45.82  by (rtac (prem1 RS wfI) 1);
   45.83  by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);