formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
authorhaftmann
Fri Aug 27 10:56:46 2010 +0200 (2010-08-27)
changeset 38795848be46708dc
parent 38794 2d638e963357
child 38796 c421cfe2eada
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
NEWS
src/HOL/Auth/Yahalom.thy
src/HOL/Boogie/Tools/boogie_tactics.ML
src/HOL/Boogie/Tools/boogie_vcs.ML
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/HOL.thy
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOL/bool.imp
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Import/proof_kernel.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Mutabelle/Mutabelle.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Orderings.thy
src/HOL/Prolog/prolog.ML
src/HOL/Set.thy
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_proof_literals.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/simpdata.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/NEWS	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/NEWS	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -104,6 +104,8 @@
     1.4      Trueprop ~> HOL.Trueprop
     1.5      True ~> HOL.True
     1.6      False ~> HOL.False
     1.7 +    op & ~> HOL.conj
     1.8 +    op | ~> HOL.disj
     1.9      op --> ~> HOL.implies
    1.10      Not ~> HOL.Not
    1.11      The ~> HOL.The
     2.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Aug 27 10:55:20 2010 +0200
     2.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Aug 27 10:56:46 2010 +0200
     2.3 @@ -197,6 +197,7 @@
     2.4  apply (erule yahalom.induct,
     2.5         drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
     2.6  apply (simp only: Says_Server_not_range analz_image_freshK_simps)
     2.7 +apply safe
     2.8  done
     2.9  
    2.10  lemma analz_insert_freshK:
     3.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Aug 27 10:55:20 2010 +0200
     3.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Fri Aug 27 10:56:46 2010 +0200
     3.3 @@ -50,11 +50,11 @@
     3.4  
     3.5  
     3.6  local
     3.7 -  fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
     3.8 +  fun explode_conj (@{term HOL.conj} $ t $ u) = explode_conj t @ explode_conj u
     3.9      | explode_conj t = [t] 
    3.10  
    3.11    fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
    3.12 -    | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
    3.13 +    | splt (ts, @{term HOL.conj} $ t $ u) = splt (ts, t) @ splt (ts, u)
    3.14      | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
    3.15      | splt (_, @{term True}) = []
    3.16      | splt tp = [tp]
     4.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Aug 27 10:55:20 2010 +0200
     4.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Aug 27 10:56:46 2010 +0200
     4.3 @@ -62,9 +62,9 @@
     4.4        | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
     4.5        | vc_of (@{term HOL.implies} $ t $ u) =
     4.6            vc_of u |> Option.map (assume t)
     4.7 -      | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
     4.8 +      | vc_of (@{term HOL.conj} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
     4.9            SOME (vc_of u |> the_default True |> assert (n, t))
    4.10 -      | vc_of (@{term "op &"} $ t $ u) =
    4.11 +      | vc_of (@{term HOL.conj} $ t $ u) =
    4.12            (case (vc_of t, vc_of u) of
    4.13              (NONE, r) => r
    4.14            | (l, NONE) => l
    4.15 @@ -74,7 +74,7 @@
    4.16  
    4.17  val prop_of_vc =
    4.18    let
    4.19 -    fun mk_conj t u = @{term "op &"} $ t $ u
    4.20 +    fun mk_conj t u = @{term HOL.conj} $ t $ u
    4.21  
    4.22      fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
    4.23        | term_of (Assert ((n, t), v)) =
     5.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 27 10:55:20 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 27 10:56:46 2010 +0200
     5.3 @@ -1952,9 +1952,9 @@
     5.4          | NONE => error "num_of_term: unsupported dvd")
     5.5    | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
     5.6        @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
     5.7 -  | fm_of_term ps vs (@{term "op &"} $ t1 $ t2) =
     5.8 +  | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
     5.9        @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
    5.10 -  | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
    5.11 +  | fm_of_term ps vs (@{term HOL.disj} $ t1 $ t2) =
    5.12        @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
    5.13    | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
    5.14        @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
    5.15 @@ -2016,7 +2016,7 @@
    5.16  
    5.17  fun term_bools acc t =
    5.18    let
    5.19 -    val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
    5.20 +    val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
    5.21        @{term "op = :: int => _"}, @{term "op < :: int => _"},
    5.22        @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
    5.23        @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
     6.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 27 10:55:20 2010 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 27 10:56:46 2010 +0200
     6.3 @@ -1996,8 +1996,8 @@
     6.4        @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2)) 
     6.5    | fm_of_term vs (@{term "op \<longleftrightarrow> :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
     6.6        @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
     6.7 -  | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
     6.8 -  | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
     6.9 +  | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
    6.10 +  | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
    6.11    | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
    6.12    | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
    6.13    | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
     7.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 27 10:55:20 2010 +0200
     7.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 27 10:56:46 2010 +0200
     7.3 @@ -5837,9 +5837,9 @@
     7.4        @{code Dvd} (HOLogic.dest_numeral t1, num_of_term vs t2)
     7.5    | fm_of_term vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
     7.6        @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
     7.7 -  | fm_of_term vs (@{term "op &"} $ t1 $ t2) =
     7.8 +  | fm_of_term vs (@{term HOL.conj} $ t1 $ t2) =
     7.9        @{code And} (fm_of_term vs t1, fm_of_term vs t2)
    7.10 -  | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
    7.11 +  | fm_of_term vs (@{term HOL.disj} $ t1 $ t2) =
    7.12        @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
    7.13    | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
    7.14        @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
     8.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 10:55:20 2010 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 10:56:46 2010 +0200
     8.3 @@ -2954,8 +2954,8 @@
     8.4  fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
     8.5  val brT = [bT, bT] ---> bT;
     8.6  val nott = @{term "Not"};
     8.7 -val conjt = @{term "op &"};
     8.8 -val disjt = @{term "op |"};
     8.9 +val conjt = @{term HOL.conj};
    8.10 +val disjt = @{term HOL.disj};
    8.11  val impt = @{term HOL.implies};
    8.12  val ifft = @{term "op = :: bool => _"}
    8.13  fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    8.14 @@ -3018,8 +3018,8 @@
    8.15      Const(@{const_name True},_) => @{code T}
    8.16    | Const(@{const_name False},_) => @{code F}
    8.17    | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
    8.18 -  | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    8.19 -  | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    8.20 +  | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    8.21 +  | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    8.22    | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    8.23    | Const(@{const_name "op ="},ty)$p$q => 
    8.24         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
     9.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Aug 27 10:55:20 2010 +0200
     9.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Fri Aug 27 10:56:46 2010 +0200
     9.3 @@ -33,12 +33,12 @@
     9.4               {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) =
     9.5  let
     9.6   fun uset (vars as (x::vs)) p = case term_of p of
     9.7 -   Const(@{const_name "op &"}, _)$ _ $ _ =>
     9.8 +   Const(@{const_name HOL.conj}, _)$ _ $ _ =>
     9.9       let
    9.10         val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    9.11         val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    9.12       in (lS@rS, Drule.binop_cong_rule b lth rth) end
    9.13 - |  Const(@{const_name "op |"}, _)$ _ $ _ =>
    9.14 + |  Const(@{const_name HOL.disj}, _)$ _ $ _ =>
    9.15       let
    9.16         val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb
    9.17         val (lS,lth) = uset vars l  val (rS, rth) = uset vars r
    9.18 @@ -122,12 +122,12 @@
    9.19  
    9.20     fun decomp_mpinf fm =
    9.21       case term_of fm of
    9.22 -       Const(@{const_name "op &"},_)$_$_ =>
    9.23 +       Const(@{const_name HOL.conj},_)$_$_ =>
    9.24          let val (p,q) = Thm.dest_binop fm
    9.25          in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
    9.26                           (Thm.cabs x p) (Thm.cabs x q))
    9.27          end
    9.28 -     | Const(@{const_name "op |"},_)$_$_ =>
    9.29 +     | Const(@{const_name HOL.disj},_)$_$_ =>
    9.30          let val (p,q) = Thm.dest_binop fm
    9.31          in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
    9.32                           (Thm.cabs x p) (Thm.cabs x q))
    9.33 @@ -181,8 +181,8 @@
    9.34     | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
    9.35     | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.36     | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    9.37 -   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    9.38 -   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    9.39 +   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
    9.40 +   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
    9.41     | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    9.42     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    9.43     | Const ("==", _) $ _ $ _ => find_args bounds tm
    10.1 --- a/src/HOL/Decision_Procs/langford.ML	Fri Aug 27 10:55:20 2010 +0200
    10.2 +++ b/src/HOL/Decision_Procs/langford.ML	Fri Aug 27 10:56:46 2010 +0200
    10.3 @@ -69,28 +69,28 @@
    10.4  val all_conjuncts = 
    10.5   let fun h acc ct = 
    10.6    case term_of ct of
    10.7 -   @{term "op &"}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
    10.8 +   @{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
    10.9    | _ => ct::acc
   10.10  in h [] end;
   10.11  
   10.12  fun conjuncts ct =
   10.13   case term_of ct of
   10.14 -  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
   10.15 +  @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
   10.16  | _ => [ct];
   10.17  
   10.18  fun fold1 f = foldr1 (uncurry f);
   10.19  
   10.20 -val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
   10.21 +val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
   10.22  
   10.23  fun mk_conj_tab th = 
   10.24   let fun h acc th = 
   10.25     case prop_of th of
   10.26 -   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
   10.27 +   @{term "Trueprop"}$(@{term HOL.conj}$p$q) => 
   10.28       h (h acc (th RS conjunct2)) (th RS conjunct1)
   10.29    | @{term "Trueprop"}$p => (p,th)::acc
   10.30  in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
   10.31  
   10.32 -fun is_conj (@{term "op &"}$_$_) = true
   10.33 +fun is_conj (@{term HOL.conj}$_$_) = true
   10.34    | is_conj _ = false;
   10.35  
   10.36  fun prove_conj tab cjs = 
   10.37 @@ -183,8 +183,8 @@
   10.38     | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.39     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.40     | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
   10.41 -   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   10.42 -   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
   10.43 +   | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
   10.44 +   | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
   10.45     | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   10.46     | Const ("==>", _) $ _ $ _ => find_args bounds tm
   10.47     | Const ("==", _) $ _ $ _ => find_args bounds tm
    11.1 --- a/src/HOL/HOL.thy	Fri Aug 27 10:55:20 2010 +0200
    11.2 +++ b/src/HOL/HOL.thy	Fri Aug 27 10:56:46 2010 +0200
    11.3 @@ -56,14 +56,14 @@
    11.4    True          :: bool
    11.5    False         :: bool
    11.6    Not           :: "bool => bool"                   ("~ _" [40] 40)
    11.7 +
    11.8 +  conj          :: "[bool, bool] => bool"           (infixr "&" 35)
    11.9 +  disj          :: "[bool, bool] => bool"           (infixr "|" 30)
   11.10    implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
   11.11  
   11.12  setup Sign.root_path
   11.13  
   11.14  consts
   11.15 -  "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
   11.16 -  "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
   11.17 -
   11.18    "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
   11.19  
   11.20  setup Sign.local_path
   11.21 @@ -89,15 +89,15 @@
   11.22  
   11.23  notation (xsymbols)
   11.24    Not  ("\<not> _" [40] 40) and
   11.25 -  "op &"  (infixr "\<and>" 35) and
   11.26 -  "op |"  (infixr "\<or>" 30) and
   11.27 +  HOL.conj  (infixr "\<and>" 35) and
   11.28 +  HOL.disj  (infixr "\<or>" 30) and
   11.29    HOL.implies  (infixr "\<longrightarrow>" 25) and
   11.30    not_equal  (infix "\<noteq>" 50)
   11.31  
   11.32  notation (HTML output)
   11.33    Not  ("\<not> _" [40] 40) and
   11.34 -  "op &"  (infixr "\<and>" 35) and
   11.35 -  "op |"  (infixr "\<or>" 30) and
   11.36 +  HOL.conj  (infixr "\<and>" 35) and
   11.37 +  HOL.disj  (infixr "\<or>" 30) and
   11.38    not_equal  (infix "\<noteq>" 50)
   11.39  
   11.40  abbreviation (iff)
   11.41 @@ -1578,7 +1578,7 @@
   11.42    val atomize_conjL = @{thm atomize_conjL}
   11.43    val atomize_disjL = @{thm atomize_disjL}
   11.44    val operator_names =
   11.45 -    [@{const_name "op |"}, @{const_name "op &"}, @{const_name Ex}]
   11.46 +    [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
   11.47  );
   11.48  *}
   11.49  
   11.50 @@ -1737,8 +1737,8 @@
   11.51    "True"    ("true")
   11.52    "False"   ("false")
   11.53    "Not"     ("Bool.not")
   11.54 -  "op |"    ("(_ orelse/ _)")
   11.55 -  "op &"    ("(_ andalso/ _)")
   11.56 +  HOL.disj    ("(_ orelse/ _)")
   11.57 +  HOL.conj    ("(_ andalso/ _)")
   11.58    "If"      ("(if _/ then _/ else _)")
   11.59  
   11.60  setup {*
   11.61 @@ -1914,7 +1914,7 @@
   11.62    (Haskell "Bool")
   11.63    (Scala "Boolean")
   11.64  
   11.65 -code_const True and False and Not and "op &" and "op |" and If
   11.66 +code_const True and False and Not and HOL.conj and HOL.disj and If
   11.67    (SML "true" and "false" and "not"
   11.68      and infixl 1 "andalso" and infixl 0 "orelse"
   11.69      and "!(if (_)/ then (_)/ else (_))")
    12.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Aug 27 10:55:20 2010 +0200
    12.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Aug 27 10:56:46 2010 +0200
    12.3 @@ -17,8 +17,8 @@
    12.4    T               > True
    12.5    F               > False
    12.6    "!"             > All
    12.7 -  "/\\"           > "op &"
    12.8 -  "\\/"           > "op |"
    12.9 +  "/\\"           > HOL.conj
   12.10 +  "\\/"           > HOL.disj
   12.11    "?"             > Ex
   12.12    "?!"            > Ex1
   12.13    "~"             > Not
    13.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Aug 27 10:55:20 2010 +0200
    13.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Aug 27 10:56:46 2010 +0200
    13.3 @@ -55,8 +55,8 @@
    13.4    ONTO    > Fun.surj
    13.5    "=" > "op ="
    13.6    "==>" > HOL.implies
    13.7 -  "/\\" > "op &"
    13.8 -  "\\/" > "op |"
    13.9 +  "/\\" > HOL.conj
   13.10 +  "\\/" > HOL.disj
   13.11    "!" > All
   13.12    "?" > Ex
   13.13    "?!" > Ex1
    14.1 --- a/src/HOL/Import/HOL/bool.imp	Fri Aug 27 10:55:20 2010 +0200
    14.2 +++ b/src/HOL/Import/HOL/bool.imp	Fri Aug 27 10:56:46 2010 +0200
    14.3 @@ -14,7 +14,7 @@
    14.4  const_maps
    14.5    "~" > "HOL.Not"
    14.6    "bool_case" > "Datatype.bool.bool_case"
    14.7 -  "\\/" > "op |"
    14.8 +  "\\/" > HOL.disj
    14.9    "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
   14.10    "T" > "HOL.True"
   14.11    "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
   14.12 @@ -30,7 +30,7 @@
   14.13    "ARB" > "HOL4Base.bool.ARB"
   14.14    "?!" > "HOL.Ex1"
   14.15    "?" > "HOL.Ex"
   14.16 -  "/\\" > "op &"
   14.17 +  "/\\" > HOL.conj
   14.18    "!" > "HOL.All"
   14.19  
   14.20  thm_maps
    15.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Fri Aug 27 10:55:20 2010 +0200
    15.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Aug 27 10:56:46 2010 +0200
    15.3 @@ -115,7 +115,7 @@
    15.4    "_10303" > "HOLLight.hollight._10303"
    15.5    "_10302" > "HOLLight.hollight._10302"
    15.6    "_0" > "0" :: "nat"
    15.7 -  "\\/" > "op |"
    15.8 +  "\\/" > HOL.disj
    15.9    "ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
   15.10    "ZIP" > "HOLLight.hollight.ZIP"
   15.11    "ZCONSTR" > "HOLLight.hollight.ZCONSTR"
   15.12 @@ -237,7 +237,7 @@
   15.13    "=" > "op ="
   15.14    "<=" > "HOLLight.hollight.<="
   15.15    "<" > "HOLLight.hollight.<"
   15.16 -  "/\\" > "op &"
   15.17 +  "/\\" > HOL.conj
   15.18    "-" > "Groups.minus" :: "nat => nat => nat"
   15.19    "," > "Product_Type.Pair"
   15.20    "+" > "Groups.plus" :: "nat => nat => nat"
    16.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Aug 27 10:55:20 2010 +0200
    16.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Aug 27 10:56:46 2010 +0200
    16.3 @@ -1205,7 +1205,7 @@
    16.4  fun non_trivial_term_consts t = fold_aterms
    16.5    (fn Const (c, _) =>
    16.6        if c = @{const_name Trueprop} orelse c = @{const_name All}
    16.7 -        orelse c = @{const_name HOL.implies} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
    16.8 +        orelse c = @{const_name HOL.implies} orelse c = @{const_name HOL.conj} orelse c = @{const_name "op ="}
    16.9        then I else insert (op =) c
   16.10      | _ => I) t [];
   16.11  
   16.12 @@ -1217,7 +1217,7 @@
   16.13                 | @{const_name HOL.implies} => insert (op =) "==>" cs
   16.14                 | @{const_name All} => cs
   16.15                 | "all" => cs
   16.16 -               | @{const_name "op &"} => cs
   16.17 +               | @{const_name HOL.conj} => cs
   16.18                 | @{const_name Trueprop} => cs
   16.19                 | _ => insert (op =) c cs)
   16.20            | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
   16.21 @@ -1521,7 +1521,7 @@
   16.22          val th1 = norm_hyps th1
   16.23          val th2 = norm_hyps th2
   16.24          val (l,r) = case concl_of th of
   16.25 -                        _ $ (Const(@{const_name "op |"},_) $ l $ r) => (l,r)
   16.26 +                        _ $ (Const(@{const_name HOL.disj},_) $ l $ r) => (l,r)
   16.27                        | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
   16.28          val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
   16.29          val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
    17.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 10:55:20 2010 +0200
    17.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 10:56:46 2010 +0200
    17.3 @@ -1356,7 +1356,7 @@
    17.4  
    17.5  val known_sos_constants =
    17.6    [@{term "op ==>"}, @{term "Trueprop"},
    17.7 -   @{term HOL.implies}, @{term "op &"}, @{term "op |"},
    17.8 +   @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
    17.9     @{term "Not"}, @{term "op = :: bool => _"},
   17.10     @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
   17.11     @{term "op = :: real => _"}, @{term "op < :: real => _"},
    18.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 10:55:20 2010 +0200
    18.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 10:56:46 2010 +0200
    18.3 @@ -439,8 +439,8 @@
    18.4    val is_req = is_binop @{cterm "op =:: real => _"}
    18.5    val is_ge = is_binop @{cterm "op <=:: real => _"}
    18.6    val is_gt = is_binop @{cterm "op <:: real => _"}
    18.7 -  val is_conj = is_binop @{cterm "op &"}
    18.8 -  val is_disj = is_binop @{cterm "op |"}
    18.9 +  val is_conj = is_binop @{cterm HOL.conj}
   18.10 +  val is_disj = is_binop @{cterm HOL.disj}
   18.11    fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
   18.12    fun disj_cases th th1 th2 = 
   18.13     let val (p,q) = Thm.dest_binop (concl th)
   18.14 @@ -484,7 +484,7 @@
   18.15      val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
   18.16      val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
   18.17      val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
   18.18 -    val th' = Drule.binop_cong_rule @{cterm "op |"} 
   18.19 +    val th' = Drule.binop_cong_rule @{cterm HOL.disj} 
   18.20       (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
   18.21       (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
   18.22      in Thm.transitive th th' 
   18.23 @@ -542,12 +542,12 @@
   18.24    let 
   18.25     val nnf_norm_conv' = 
   18.26       nnf_conv then_conv 
   18.27 -     literals_conv [@{term "op &"}, @{term "op |"}] [] 
   18.28 +     literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
   18.29       (Conv.cache_conv 
   18.30         (first_conv [real_lt_conv, real_le_conv, 
   18.31                      real_eq_conv, real_not_lt_conv, 
   18.32                      real_not_le_conv, real_not_eq_conv, all_conv]))
   18.33 -  fun absremover ct = (literals_conv [@{term "op &"}, @{term "op |"}] [] 
   18.34 +  fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
   18.35                    (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
   18.36          try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
   18.37    val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
    19.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Fri Aug 27 10:55:20 2010 +0200
    19.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Fri Aug 27 10:56:46 2010 +0200
    19.3 @@ -4,7 +4,7 @@
    19.4  begin
    19.5  
    19.6  ML {*
    19.7 -val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
    19.8 +val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
    19.9  
   19.10  val forbidden =
   19.11   [(@{const_name Power.power}, "'a"),
    20.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 10:55:20 2010 +0200
    20.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 10:56:46 2010 +0200
    20.3 @@ -187,7 +187,7 @@
    20.4  val nitpick_mtd = ("nitpick", invoke_nitpick)
    20.5  *)
    20.6  
    20.7 -val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}]
    20.8 +val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
    20.9  
   20.10  val forbidden =
   20.11   [(* (@{const_name "power"}, "'a"), *)
    21.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Aug 27 10:55:20 2010 +0200
    21.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Aug 27 10:56:46 2010 +0200
    21.3 @@ -1200,7 +1200,7 @@
    21.4            (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
    21.5      val tnames = Datatype_Prop.make_tnames recTs;
    21.6      val zs = Name.variant_list tnames (replicate (length descr'') "z");
    21.7 -    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
    21.8 +    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
    21.9        (map (fn ((((i, _), T), tname), z) =>
   21.10          make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
   21.11          (descr'' ~~ recTs ~~ tnames ~~ zs)));
   21.12 @@ -1215,7 +1215,7 @@
   21.13          map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
   21.14            HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
   21.15              (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
   21.16 -    val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
   21.17 +    val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
   21.18        (map (fn ((((i, _), T), tname), z) =>
   21.19          make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
   21.20          (descr'' ~~ recTs ~~ tnames ~~ zs)));
   21.21 @@ -1225,7 +1225,7 @@
   21.22        (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
   21.23         map mk_permT dt_atomTs) @ [("z", fsT')];
   21.24      val aux_ind_Ts = rev (map snd aux_ind_vars);
   21.25 -    val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
   21.26 +    val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
   21.27        (map (fn (((i, _), T), tname) =>
   21.28          HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
   21.29            fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
    22.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Aug 27 10:55:20 2010 +0200
    22.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Aug 27 10:56:46 2010 +0200
    22.3 @@ -71,7 +71,7 @@
    22.4    | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
    22.5    | add_binders thy i _ bs = bs;
    22.6  
    22.7 -fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
    22.8 +fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
    22.9        Const (name, _) =>
   22.10          if member (op =) names name then SOME (f p q) else NONE
   22.11      | _ => NONE)
   22.12 @@ -89,7 +89,7 @@
   22.13  (* where "id" protects the subformula from simplification            *)
   22.14  (*********************************************************************)
   22.15  
   22.16 -fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
   22.17 +fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
   22.18        (case head_of p of
   22.19           Const (name, _) =>
   22.20             if member (op =) names name then SOME (HOLogic.mk_conj (p,
    23.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Aug 27 10:55:20 2010 +0200
    23.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Aug 27 10:56:46 2010 +0200
    23.3 @@ -76,7 +76,7 @@
    23.4    | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
    23.5    | add_binders thy i _ bs = bs;
    23.6  
    23.7 -fun split_conj f names (Const (@{const_name "op &"}, _) $ p $ q) _ = (case head_of p of
    23.8 +fun split_conj f names (Const (@{const_name HOL.conj}, _) $ p $ q) _ = (case head_of p of
    23.9        Const (name, _) =>
   23.10          if member (op =) names name then SOME (f p q) else NONE
   23.11      | _ => NONE)
   23.12 @@ -94,7 +94,7 @@
   23.13  (* where "id" protects the subformula from simplification            *)
   23.14  (*********************************************************************)
   23.15  
   23.16 -fun inst_conj_all names ps pis (Const (@{const_name "op &"}, _) $ p $ q) _ =
   23.17 +fun inst_conj_all names ps pis (Const (@{const_name HOL.conj}, _) $ p $ q) _ =
   23.18        (case head_of p of
   23.19           Const (name, _) =>
   23.20             if member (op =) names name then SOME (HOLogic.mk_conj (p,
    24.1 --- a/src/HOL/Orderings.thy	Fri Aug 27 10:55:20 2010 +0200
    24.2 +++ b/src/HOL/Orderings.thy	Fri Aug 27 10:56:46 2010 +0200
    24.3 @@ -641,7 +641,7 @@
    24.4    val All_binder = Syntax.binder_name @{const_syntax All};
    24.5    val Ex_binder = Syntax.binder_name @{const_syntax Ex};
    24.6    val impl = @{const_syntax HOL.implies};
    24.7 -  val conj = @{const_syntax "op &"};
    24.8 +  val conj = @{const_syntax HOL.conj};
    24.9    val less = @{const_syntax less};
   24.10    val less_eq = @{const_syntax less_eq};
   24.11  
    25.1 --- a/src/HOL/Prolog/prolog.ML	Fri Aug 27 10:55:20 2010 +0200
    25.2 +++ b/src/HOL/Prolog/prolog.ML	Fri Aug 27 10:56:46 2010 +0200
    25.3 @@ -11,12 +11,12 @@
    25.4  
    25.5  fun isD t = case t of
    25.6      Const(@{const_name Trueprop},_)$t     => isD t
    25.7 -  | Const(@{const_name "op &"}  ,_)$l$r     => isD l andalso isD r
    25.8 +  | Const(@{const_name HOL.conj}  ,_)$l$r     => isD l andalso isD r
    25.9    | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
   25.10    | Const(   "==>",_)$l$r     => isG l andalso isD r
   25.11    | Const(@{const_name All},_)$Abs(s,_,t) => isD t
   25.12    | Const("all",_)$Abs(s,_,t) => isD t
   25.13 -  | Const(@{const_name "op |"},_)$_$_       => false
   25.14 +  | Const(@{const_name HOL.disj},_)$_$_       => false
   25.15    | Const(@{const_name Ex} ,_)$_          => false
   25.16    | Const(@{const_name Not},_)$_          => false
   25.17    | Const(@{const_name True},_)           => false
   25.18 @@ -30,8 +30,8 @@
   25.19  and
   25.20      isG t = case t of
   25.21      Const(@{const_name Trueprop},_)$t     => isG t
   25.22 -  | Const(@{const_name "op &"}  ,_)$l$r     => isG l andalso isG r
   25.23 -  | Const(@{const_name "op |"}  ,_)$l$r     => isG l andalso isG r
   25.24 +  | Const(@{const_name HOL.conj}  ,_)$l$r     => isG l andalso isG r
   25.25 +  | Const(@{const_name HOL.disj}  ,_)$l$r     => isG l andalso isG r
   25.26    | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
   25.27    | Const(   "==>",_)$l$r     => isD l andalso isG r
   25.28    | Const(@{const_name All},_)$Abs(_,_,t) => isG t
   25.29 @@ -53,7 +53,7 @@
   25.30      fun at  thm = case concl_of thm of
   25.31        _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
   25.32          (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
   25.33 -    | _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   25.34 +    | _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   25.35      | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
   25.36      | _                             => [thm]
   25.37  in map zero_var_indexes (at thm) end;
    26.1 --- a/src/HOL/Set.thy	Fri Aug 27 10:55:20 2010 +0200
    26.2 +++ b/src/HOL/Set.thy	Fri Aug 27 10:56:46 2010 +0200
    26.3 @@ -220,7 +220,7 @@
    26.4    val All_binder = Syntax.binder_name @{const_syntax All};
    26.5    val Ex_binder = Syntax.binder_name @{const_syntax Ex};
    26.6    val impl = @{const_syntax HOL.implies};
    26.7 -  val conj = @{const_syntax "op &"};
    26.8 +  val conj = @{const_syntax HOL.conj};
    26.9    val sbset = @{const_syntax subset};
   26.10    val sbset_eq = @{const_syntax subset_eq};
   26.11  
   26.12 @@ -269,7 +269,7 @@
   26.13      fun setcompr_tr [e, idts, b] =
   26.14        let
   26.15          val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
   26.16 -        val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
   26.17 +        val P = Syntax.const @{const_syntax HOL.conj} $ eq $ b;
   26.18          val exP = ex_tr [idts, P];
   26.19        in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
   26.20  
   26.21 @@ -288,7 +288,7 @@
   26.22    fun setcompr_tr' [Abs (abs as (_, _, P))] =
   26.23      let
   26.24        fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
   26.25 -        | check (Const (@{const_syntax "op &"}, _) $
   26.26 +        | check (Const (@{const_syntax HOL.conj}, _) $
   26.27                (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
   26.28              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
   26.29              subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
   26.30 @@ -305,7 +305,7 @@
   26.31            val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
   26.32          in
   26.33            case t of
   26.34 -            Const (@{const_syntax "op &"}, _) $
   26.35 +            Const (@{const_syntax HOL.conj}, _) $
   26.36                (Const (@{const_syntax Set.member}, _) $
   26.37                  (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
   26.38              if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
    27.1 --- a/src/HOL/Statespace/state_fun.ML	Fri Aug 27 10:55:20 2010 +0200
    27.2 +++ b/src/HOL/Statespace/state_fun.ML	Fri Aug 27 10:56:46 2010 +0200
    27.3 @@ -53,7 +53,7 @@
    27.4  val lazy_conj_simproc =
    27.5    Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
    27.6      (fn thy => fn ss => fn t =>
    27.7 -      (case t of (Const (@{const_name "op &"},_)$P$Q) => 
    27.8 +      (case t of (Const (@{const_name HOL.conj},_)$P$Q) => 
    27.9           let
   27.10              val P_P' = Simplifier.rewrite ss (cterm_of thy P);
   27.11              val P' = P_P' |> prop_of |> Logic.dest_equals |> #2 
    28.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Aug 27 10:55:20 2010 +0200
    28.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Aug 27 10:56:46 2010 +0200
    28.3 @@ -120,8 +120,8 @@
    28.4  fun split_conj_thm th =
    28.5    ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
    28.6  
    28.7 -val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"});
    28.8 -val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"});
    28.9 +val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
   28.10 +val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
   28.11  
   28.12  fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
   28.13  
    29.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Aug 27 10:55:20 2010 +0200
    29.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Aug 27 10:56:46 2010 +0200
    29.3 @@ -70,7 +70,7 @@
    29.4            val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
    29.5          in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
    29.6            (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
    29.7 -           foldr1 (HOLogic.mk_binop @{const_name "op &"})
    29.8 +           foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
    29.9               (map HOLogic.mk_eq (frees ~~ frees')))))
   29.10          end;
   29.11    in
   29.12 @@ -149,7 +149,7 @@
   29.13      val prems = maps (fn ((i, (_, _, constrs)), T) =>
   29.14        map (make_ind_prem i T) constrs) (descr' ~~ recTs);
   29.15      val tnames = make_tnames recTs;
   29.16 -    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
   29.17 +    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
   29.18        (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
   29.19          (descr' ~~ recTs ~~ tnames)))
   29.20  
    30.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Aug 27 10:55:20 2010 +0200
    30.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Fri Aug 27 10:56:46 2010 +0200
    30.3 @@ -99,7 +99,7 @@
    30.4          if member (op =) is i then SOME
    30.5            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
    30.6          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
    30.7 -    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
    30.8 +    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
    30.9        (map (fn ((((i, _), T), U), tname) =>
   30.10          make_pred i U T (mk_proj i is r) (Free (tname, T)))
   30.11            (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
    31.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Aug 27 10:55:20 2010 +0200
    31.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Aug 27 10:56:46 2010 +0200
    31.3 @@ -148,7 +148,7 @@
    31.4      val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
    31.5      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    31.6        let
    31.7 -        val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
    31.8 +        val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
    31.9            = Term.strip_qnt_body @{const_name Ex} c
   31.10        in cons r o cons l end
   31.11    in
   31.12 @@ -185,7 +185,7 @@
   31.13      val vs = Term.strip_qnt_vars @{const_name Ex} c
   31.14  
   31.15      (* FIXME: throw error "dest_call" for malformed terms *)
   31.16 -    val (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
   31.17 +    val (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name "op ="}, _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
   31.18        = Term.strip_qnt_body @{const_name Ex} c
   31.19      val (p, l') = dest_inj sk l
   31.20      val (q, r') = dest_inj sk r
    32.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Fri Aug 27 10:55:20 2010 +0200
    32.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Fri Aug 27 10:56:46 2010 +0200
    32.3 @@ -130,8 +130,8 @@
    32.4                        [Type (@{type_name fun}, [_, @{typ bool}]), _]))
    32.5           $ t1 $ t2 =>
    32.6           Subset (to_R_rep Ts t1, to_R_rep Ts t2)
    32.7 -       | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
    32.8 -       | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
    32.9 +       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
   32.10 +       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
   32.11         | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
   32.12         | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   32.13         | Free _ => raise SAME ()
   32.14 @@ -173,10 +173,10 @@
   32.15           to_R_rep Ts (eta_expand Ts t 1)
   32.16         | Const (@{const_name ord_class.less_eq}, _) =>
   32.17           to_R_rep Ts (eta_expand Ts t 2)
   32.18 -       | @{const "op &"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   32.19 -       | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
   32.20 -       | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   32.21 -       | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
   32.22 +       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   32.23 +       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
   32.24 +       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   32.25 +       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
   32.26         | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   32.27         | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   32.28         | Const (@{const_name bot_class.bot},
    33.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 27 10:55:20 2010 +0200
    33.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 27 10:56:46 2010 +0200
    33.3 @@ -386,13 +386,13 @@
    33.4      if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
    33.5    | strip_connective _ t = [t]
    33.6  fun strip_any_connective (t as (t0 $ _ $ _)) =
    33.7 -    if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
    33.8 +    if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
    33.9        (strip_connective t0 t, t0)
   33.10      else
   33.11        ([t], @{const Not})
   33.12    | strip_any_connective t = ([t], @{const Not})
   33.13 -val conjuncts_of = strip_connective @{const "op &"}
   33.14 -val disjuncts_of = strip_connective @{const "op |"}
   33.15 +val conjuncts_of = strip_connective @{const HOL.conj}
   33.16 +val disjuncts_of = strip_connective @{const HOL.disj}
   33.17  
   33.18  (* When you add constants to these lists, make sure to handle them in
   33.19     "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
   33.20 @@ -409,8 +409,8 @@
   33.21     (@{const_name All}, 1),
   33.22     (@{const_name Ex}, 1),
   33.23     (@{const_name "op ="}, 1),
   33.24 -   (@{const_name "op &"}, 2),
   33.25 -   (@{const_name "op |"}, 2),
   33.26 +   (@{const_name HOL.conj}, 2),
   33.27 +   (@{const_name HOL.disj}, 2),
   33.28     (@{const_name HOL.implies}, 2),
   33.29     (@{const_name If}, 3),
   33.30     (@{const_name Let}, 2),
   33.31 @@ -2148,8 +2148,8 @@
   33.32            fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
   33.33                Const (@{const_name Ex}, T1)
   33.34                $ Abs (s2, T2, repair_rec (j + 1) t2')
   33.35 -            | repair_rec j (@{const "op &"} $ t1 $ t2) =
   33.36 -              @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
   33.37 +            | repair_rec j (@{const HOL.conj} $ t1 $ t2) =
   33.38 +              @{const HOL.conj} $ repair_rec j t1 $ repair_rec j t2
   33.39              | repair_rec j t =
   33.40                let val (head, args) = strip_comb t in
   33.41                  if head = Bound j then
    34.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Aug 27 10:55:20 2010 +0200
    34.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Aug 27 10:56:46 2010 +0200
    34.3 @@ -777,7 +777,7 @@
    34.4             $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
    34.5             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
    34.6           | (t0 as Const (@{const_name Ex}, _))
    34.7 -           $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
    34.8 +           $ Abs (s', T', (t10 as @{const HOL.conj}) $ (t11 $ Bound 0) $ t12) =>
    34.9             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   34.10           | Const (@{const_name Let}, _) $ t1 $ t2 =>
   34.11             do_term (betapply (t2, t1)) accum
   34.12 @@ -883,8 +883,8 @@
   34.13             | (t0 as Const (s0, _)) $ t1 $ t2 =>
   34.14               if s0 = @{const_name "==>"} orelse
   34.15                  s0 = @{const_name Pure.conjunction} orelse
   34.16 -                s0 = @{const_name "op &"} orelse
   34.17 -                s0 = @{const_name "op |"} orelse
   34.18 +                s0 = @{const_name HOL.conj} orelse
   34.19 +                s0 = @{const_name HOL.disj} orelse
   34.20                  s0 = @{const_name HOL.implies} then
   34.21                 let
   34.22                   val impl = (s0 = @{const_name "==>"} orelse
   34.23 @@ -975,7 +975,7 @@
   34.24              do_all t0 s0 T1 t1 accum
   34.25            | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
   34.26              consider_general_equals mdata true x t1 t2 accum
   34.27 -          | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
   34.28 +          | (t0 as @{const HOL.conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
   34.29            | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   34.30            | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
   34.31                               \do_formula", [t])
    35.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Aug 27 10:55:20 2010 +0200
    35.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri Aug 27 10:56:46 2010 +0200
    35.3 @@ -518,9 +518,9 @@
    35.4          | (Const (@{const_name "op ="}, T), [t1]) =>
    35.5            Op1 (SingletonSet, range_type T, Any, sub t1)
    35.6          | (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
    35.7 -        | (Const (@{const_name "op &"}, _), [t1, t2]) =>
    35.8 +        | (Const (@{const_name HOL.conj}, _), [t1, t2]) =>
    35.9            Op2 (And, bool_T, Any, sub' t1, sub' t2)
   35.10 -        | (Const (@{const_name "op |"}, _), [t1, t2]) =>
   35.11 +        | (Const (@{const_name HOL.disj}, _), [t1, t2]) =>
   35.12            Op2 (Or, bool_T, Any, sub t1, sub t2)
   35.13          | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
   35.14            Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
    36.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Aug 27 10:55:20 2010 +0200
    36.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Aug 27 10:56:46 2010 +0200
    36.3 @@ -211,11 +211,11 @@
    36.4          do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
    36.5        | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
    36.6          do_equals new_Ts old_Ts s0 T0 t1 t2
    36.7 -      | @{const "op &"} $ t1 $ t2 =>
    36.8 -        @{const "op &"} $ do_term new_Ts old_Ts polar t1
    36.9 +      | @{const HOL.conj} $ t1 $ t2 =>
   36.10 +        @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
   36.11          $ do_term new_Ts old_Ts polar t2
   36.12 -      | @{const "op |"} $ t1 $ t2 =>
   36.13 -        @{const "op |"} $ do_term new_Ts old_Ts polar t1
   36.14 +      | @{const HOL.disj} $ t1 $ t2 =>
   36.15 +        @{const HOL.disj} $ do_term new_Ts old_Ts polar t1
   36.16          $ do_term new_Ts old_Ts polar t2
   36.17        | @{const HOL.implies} $ t1 $ t2 =>
   36.18          @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   36.19 @@ -449,7 +449,7 @@
   36.20  (** Destruction of universal and existential equalities **)
   36.21  
   36.22  fun curry_assms (@{const "==>"} $ (@{const Trueprop}
   36.23 -                                   $ (@{const "op &"} $ t1 $ t2)) $ t3) =
   36.24 +                                   $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
   36.25      curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
   36.26    | curry_assms (@{const "==>"} $ t1 $ t2) =
   36.27      @{const "==>"} $ curry_assms t1 $ curry_assms t2
   36.28 @@ -604,9 +604,9 @@
   36.29            do_quantifier s0 T0 s1 T1 t1
   36.30          | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
   36.31            do_quantifier s0 T0 s1 T1 t1
   36.32 -        | @{const "op &"} $ t1 $ t2 =>
   36.33 +        | @{const HOL.conj} $ t1 $ t2 =>
   36.34            s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
   36.35 -        | @{const "op |"} $ t1 $ t2 =>
   36.36 +        | @{const HOL.disj} $ t1 $ t2 =>
   36.37            s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
   36.38          | @{const HOL.implies} $ t1 $ t2 =>
   36.39            @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   36.40 @@ -620,8 +620,8 @@
   36.41              let
   36.42                val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   36.43                val (pref, connective) =
   36.44 -                if gfp then (lbfp_prefix, @{const "op |"})
   36.45 -                else (ubfp_prefix, @{const "op &"})
   36.46 +                if gfp then (lbfp_prefix, @{const HOL.disj})
   36.47 +                else (ubfp_prefix, @{const HOL.conj})
   36.48                fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
   36.49                             |> aux ss Ts js skolemizable polar
   36.50                fun neg () = Const (pref ^ s, T)
   36.51 @@ -1105,7 +1105,7 @@
   36.52    case t of
   36.53      (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
   36.54      (case t1 of
   36.55 -       (t10 as @{const "op &"}) $ t11 $ t12 =>
   36.56 +       (t10 as @{const HOL.conj}) $ t11 $ t12 =>
   36.57         t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
   36.58             $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
   36.59       | (t10 as @{const Not}) $ t11 =>
   36.60 @@ -1118,7 +1118,7 @@
   36.61           t0 $ Abs (s, T1, distribute_quantifiers t1))
   36.62    | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
   36.63      (case distribute_quantifiers t1 of
   36.64 -       (t10 as @{const "op |"}) $ t11 $ t12 =>
   36.65 +       (t10 as @{const HOL.disj}) $ t11 $ t12 =>
   36.66         t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
   36.67             $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
   36.68       | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
    37.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Aug 27 10:55:20 2010 +0200
    37.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Aug 27 10:56:46 2010 +0200
    37.3 @@ -405,7 +405,7 @@
    37.4  (* general syntactic functions *)
    37.5  
    37.6  (*Like dest_conj, but flattens conjunctions however nested*)
    37.7 -fun conjuncts_aux (Const (@{const_name "op &"}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    37.8 +fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
    37.9    | conjuncts_aux t conjs = t::conjs;
   37.10  
   37.11  fun conjuncts t = conjuncts_aux t [];
    38.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Aug 27 10:55:20 2010 +0200
    38.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Aug 27 10:56:46 2010 +0200
    38.3 @@ -524,7 +524,7 @@
    38.4  
    38.5  fun dest_conjunct_prem th =
    38.6    case HOLogic.dest_Trueprop (prop_of th) of
    38.7 -    (Const (@{const_name "op &"}, _) $ t $ t') =>
    38.8 +    (Const (@{const_name HOL.conj}, _) $ t $ t') =>
    38.9        dest_conjunct_prem (th RS @{thm conjunct1})
   38.10          @ dest_conjunct_prem (th RS @{thm conjunct2})
   38.11      | _ => [th]
    39.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Aug 27 10:55:20 2010 +0200
    39.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Aug 27 10:56:46 2010 +0200
    39.3 @@ -221,8 +221,8 @@
    39.4     @{const_name HOL.implies},
    39.5     @{const_name All},
    39.6     @{const_name Ex}, 
    39.7 -   @{const_name "op &"},
    39.8 -   @{const_name "op |"}]
    39.9 +   @{const_name HOL.conj},
   39.10 +   @{const_name HOL.disj}]
   39.11  
   39.12  fun special_cases (c, T) = member (op =) [
   39.13    @{const_name Product_Type.Unity},
    40.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Aug 27 10:55:20 2010 +0200
    40.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Aug 27 10:56:46 2010 +0200
    40.3 @@ -89,8 +89,8 @@
    40.4  fun is_compound ((Const (@{const_name Not}, _)) $ t) =
    40.5      error "is_compound: Negation should not occur; preprocessing is defect"
    40.6    | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
    40.7 -  | is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
    40.8 -  | is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
    40.9 +  | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
   40.10 +  | is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
   40.11      error "is_compound: Conjunction should not occur; preprocessing is defect"
   40.12    | is_compound _ = false
   40.13  
   40.14 @@ -250,7 +250,7 @@
   40.15  
   40.16  fun split_conjs thy t =
   40.17    let 
   40.18 -    fun split_conjunctions (Const (@{const_name "op &"}, _) $ t1 $ t2) =
   40.19 +    fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
   40.20      (split_conjunctions t1) @ (split_conjunctions t2)
   40.21      | split_conjunctions t = [t]
   40.22    in
    41.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 10:55:20 2010 +0200
    41.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 10:56:46 2010 +0200
    41.3 @@ -28,7 +28,7 @@
    41.4     @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    41.5     @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    41.6     @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
    41.7 -   @{term "op &"}, @{term "op |"}, @{term HOL.implies}, 
    41.8 +   @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, 
    41.9     @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
   41.10     @{term "op < :: int => _"}, @{term "op < :: nat => _"},
   41.11     @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
   41.12 @@ -120,8 +120,8 @@
   41.13  
   41.14  fun whatis x ct =
   41.15  ( case (term_of ct) of
   41.16 -  Const(@{const_name "op &"},_)$_$_ => And (Thm.dest_binop ct)
   41.17 -| Const (@{const_name "op |"},_)$_$_ => Or (Thm.dest_binop ct)
   41.18 +  Const(@{const_name HOL.conj},_)$_$_ => And (Thm.dest_binop ct)
   41.19 +| Const (@{const_name HOL.disj},_)$_$_ => Or (Thm.dest_binop ct)
   41.20  | Const (@{const_name "op ="},_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
   41.21  | Const (@{const_name Not},_) $ (Const (@{const_name "op ="},_)$y$_) =>
   41.22    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
   41.23 @@ -353,8 +353,8 @@
   41.24      then (ins (dest_number c) acc, dacc) else (acc,dacc)
   41.25    | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
   41.26      if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
   41.27 -  | Const(@{const_name "op &"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   41.28 -  | Const(@{const_name "op |"},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   41.29 +  | Const(@{const_name HOL.conj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   41.30 +  | Const(@{const_name HOL.disj},_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   41.31    | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   41.32    | _ => (acc, dacc)
   41.33    val (cs,ds) = h ([],[]) p
   41.34 @@ -382,8 +382,8 @@
   41.35      end
   41.36    fun unit_conv t =
   41.37     case (term_of t) of
   41.38 -   Const(@{const_name "op &"},_)$_$_ => Conv.binop_conv unit_conv t
   41.39 -  | Const(@{const_name "op |"},_)$_$_ => Conv.binop_conv unit_conv t
   41.40 +   Const(@{const_name HOL.conj},_)$_$_ => Conv.binop_conv unit_conv t
   41.41 +  | Const(@{const_name HOL.disj},_)$_$_ => Conv.binop_conv unit_conv t
   41.42    | Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t
   41.43    | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   41.44      if x=y andalso member (op =)
   41.45 @@ -569,7 +569,7 @@
   41.46  fun add_bools t =
   41.47    let
   41.48      val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
   41.49 -      @{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
   41.50 +      @{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
   41.51        @{term "Not"}, @{term "All :: (int => _) => _"},
   41.52        @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
   41.53      val is_op = member (op =) ops;
   41.54 @@ -612,9 +612,9 @@
   41.55  
   41.56  fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
   41.57    | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
   41.58 -  | fm_of_term ps vs (Const (@{const_name "op &"}, _) $ t1 $ t2) =
   41.59 +  | fm_of_term ps vs (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
   41.60        Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
   41.61 -  | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
   41.62 +  | fm_of_term ps vs (Const (@{const_name HOL.disj}, _) $ t1 $ t2) =
   41.63        Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
   41.64    | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
   41.65        Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
    42.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Fri Aug 27 10:55:20 2010 +0200
    42.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Fri Aug 27 10:56:46 2010 +0200
    42.3 @@ -25,7 +25,7 @@
    42.4     case (term_of p) of
    42.5      Const(s,T)$_$_ => 
    42.6         if domain_type T = HOLogic.boolT
    42.7 -          andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
    42.8 +          andalso member (op =) [@{const_name HOL.conj}, @{const_name HOL.disj},
    42.9              @{const_name HOL.implies}, @{const_name "op ="}] s
   42.10         then binop_conv (conv env) p 
   42.11         else atcv env p
    43.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Aug 27 10:55:20 2010 +0200
    43.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Aug 27 10:56:46 2010 +0200
    43.3 @@ -485,7 +485,7 @@
    43.4         end
    43.5  
    43.6    | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
    43.7 -      (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
    43.8 +      (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
    43.9          (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
   43.10       Const (@{const_name Ex1}, ty') $ t') =>
   43.11         let
    44.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Aug 27 10:55:20 2010 +0200
    44.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Aug 27 10:56:46 2010 +0200
    44.3 @@ -159,8 +159,8 @@
    44.4  fun conn @{const_name True} = SOME "true"
    44.5    | conn @{const_name False} = SOME "false"
    44.6    | conn @{const_name Not} = SOME "not"
    44.7 -  | conn @{const_name "op &"} = SOME "and"
    44.8 -  | conn @{const_name "op |"} = SOME "or"
    44.9 +  | conn @{const_name HOL.conj} = SOME "and"
   44.10 +  | conn @{const_name HOL.disj} = SOME "or"
   44.11    | conn @{const_name HOL.implies} = SOME "implies"
   44.12    | conn @{const_name "op ="} = SOME "iff"
   44.13    | conn @{const_name If} = SOME "if_then_else"
    45.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Aug 27 10:55:20 2010 +0200
    45.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Aug 27 10:56:46 2010 +0200
    45.3 @@ -216,8 +216,8 @@
    45.4      (Sym ("true", _), []) => SOME mk_true
    45.5    | (Sym ("false", _), []) => SOME mk_false
    45.6    | (Sym ("not", _), [ct]) => SOME (mk_not ct)
    45.7 -  | (Sym ("and", _), _) => SOME (mk_nary @{cterm "op &"} mk_true cts)
    45.8 -  | (Sym ("or", _), _) => SOME (mk_nary @{cterm "op |"} mk_false cts)
    45.9 +  | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
   45.10 +  | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
   45.11    | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
   45.12    | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
   45.13    | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
    46.1 --- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Fri Aug 27 10:55:20 2010 +0200
    46.2 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Fri Aug 27 10:56:46 2010 +0200
    46.3 @@ -62,14 +62,14 @@
    46.4  val is_neg = (fn @{term Not} $ _ => true | _ => false)
    46.5  fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
    46.6  val is_dneg = is_neg' is_neg
    46.7 -val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
    46.8 -val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
    46.9 +val is_conj = (fn @{term HOL.conj} $ _ $ _ => true | _ => false)
   46.10 +val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
   46.11  
   46.12  fun dest_disj_term' f = (fn
   46.13 -    @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
   46.14 +    @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
   46.15    | _ => NONE)
   46.16  
   46.17 -val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
   46.18 +val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
   46.19  val dest_disj_term =
   46.20    dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
   46.21  
   46.22 @@ -202,11 +202,11 @@
   46.23      | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
   46.24      | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
   46.25  
   46.26 -  fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
   46.27 +  fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
   46.28      | dest_conj t = raise TERM ("dest_conj", [t])
   46.29  
   46.30    val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
   46.31 -  fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
   46.32 +  fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
   46.33      | dest_disj t = raise TERM ("dest_disj", [t])
   46.34  
   46.35    val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
    47.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Aug 27 10:55:20 2010 +0200
    47.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Aug 27 10:56:46 2010 +0200
    47.3 @@ -298,13 +298,13 @@
    47.4      let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
    47.5      in
    47.6        (case Thm.term_of ct1 of
    47.7 -        @{term Not} $ (@{term "op &"} $ _ $ _) =>
    47.8 +        @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
    47.9            prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
   47.10 -      | @{term "op &"} $ _ $ _ =>
   47.11 +      | @{term HOL.conj} $ _ $ _ =>
   47.12            prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
   47.13 -      | @{term Not} $ (@{term "op |"} $ _ $ _) =>
   47.14 +      | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
   47.15            prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
   47.16 -      | @{term "op |"} $ _ $ _ =>
   47.17 +      | @{term HOL.disj} $ _ $ _ =>
   47.18            prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
   47.19        | Const (@{const_name distinct}, _) $ _ =>
   47.20            let
   47.21 @@ -477,8 +477,8 @@
   47.22  
   47.23    fun mono f (cp as (cl, _)) =
   47.24      (case Term.head_of (Thm.term_of cl) of
   47.25 -      @{term "op &"} => prove_nary L.is_conj (prove_eq_exn f)
   47.26 -    | @{term "op |"} => prove_nary L.is_disj (prove_eq_exn f)
   47.27 +      @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
   47.28 +    | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
   47.29      | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
   47.30      | _ => prove (prove_eq_safe f)) cp
   47.31  in
    48.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Aug 27 10:55:20 2010 +0200
    48.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Fri Aug 27 10:56:46 2010 +0200
    48.3 @@ -196,8 +196,8 @@
    48.4        | @{term True} => pair ct
    48.5        | @{term False} => pair ct
    48.6        | @{term Not} $ _ => abstr1 cvs ct
    48.7 -      | @{term "op &"} $ _ $ _ => abstr2 cvs ct
    48.8 -      | @{term "op |"} $ _ $ _ => abstr2 cvs ct
    48.9 +      | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
   48.10 +      | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
   48.11        | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
   48.12        | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
   48.13        | Const (@{const_name distinct}, _) $ _ =>
    49.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 27 10:55:20 2010 +0200
    49.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 27 10:56:46 2010 +0200
    49.3 @@ -68,8 +68,8 @@
    49.4          (*Universal quant: insert a free variable into body and continue*)
    49.5          let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    49.6          in dec_sko (subst_bound (Free(fname,T), p)) rhss end
    49.7 -      | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    49.8 -      | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    49.9 +      | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
   49.10 +      | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
   49.11        | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
   49.12        | dec_sko _ rhss = rhss
   49.13    in  dec_sko (prop_of th) []  end;
    50.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Aug 27 10:55:20 2010 +0200
    50.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Fri Aug 27 10:56:46 2010 +0200
    50.3 @@ -95,8 +95,8 @@
    50.4    Symtab.make [(@{type_name Product_Type.prod}, "prod"),
    50.5                 (@{type_name Sum_Type.sum}, "sum"),
    50.6                 (@{const_name "op ="}, "equal"),
    50.7 -               (@{const_name "op &"}, "and"),
    50.8 -               (@{const_name "op |"}, "or"),
    50.9 +               (@{const_name HOL.conj}, "and"),
   50.10 +               (@{const_name HOL.disj}, "or"),
   50.11                 (@{const_name HOL.implies}, "implies"),
   50.12                 (@{const_name Set.member}, "member"),
   50.13                 (@{const_name fequal}, "fequal"),
   50.14 @@ -430,7 +430,7 @@
   50.15  
   50.16  fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   50.17      literals_of_term1 args thy P
   50.18 -  | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
   50.19 +  | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
   50.20      literals_of_term1 (literals_of_term1 args thy P) thy Q
   50.21    | literals_of_term1 (lits, ts) thy P =
   50.22      let val ((pred, ts'), pol) = predicate_of thy (P, true) in
    51.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 10:55:20 2010 +0200
    51.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 10:56:46 2010 +0200
    51.3 @@ -159,8 +159,8 @@
    51.4          do_quantifier (pos = SOME false) body_t
    51.5        | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
    51.6          do_quantifier (pos = SOME true) body_t
    51.7 -      | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
    51.8 -      | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
    51.9 +      | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   51.10 +      | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   51.11        | @{const HOL.implies} $ t1 $ t2 =>
   51.12          do_formula (flip pos) t1 #> do_formula pos t2
   51.13        | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
   51.14 @@ -545,8 +545,8 @@
   51.15          do_formula (not pos) t1 andalso
   51.16          (t2 = @{const False} orelse do_formula pos t2)
   51.17        | (_, @{const Not} $ t1) => do_formula (not pos) t1
   51.18 -      | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   51.19 -      | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   51.20 +      | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   51.21 +      | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
   51.22        | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
   51.23        | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
   51.24        | _ => false
    52.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Aug 27 10:55:20 2010 +0200
    52.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Aug 27 10:56:46 2010 +0200
    52.3 @@ -70,11 +70,11 @@
    52.4    | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    52.5      Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
    52.6    | negate_term (@{const HOL.implies} $ t1 $ t2) =
    52.7 -    @{const "op &"} $ t1 $ negate_term t2
    52.8 -  | negate_term (@{const "op &"} $ t1 $ t2) =
    52.9 -    @{const "op |"} $ negate_term t1 $ negate_term t2
   52.10 -  | negate_term (@{const "op |"} $ t1 $ t2) =
   52.11 -    @{const "op &"} $ negate_term t1 $ negate_term t2
   52.12 +    @{const HOL.conj} $ t1 $ negate_term t2
   52.13 +  | negate_term (@{const HOL.conj} $ t1 $ t2) =
   52.14 +    @{const HOL.disj} $ negate_term t1 $ negate_term t2
   52.15 +  | negate_term (@{const HOL.disj} $ t1 $ t2) =
   52.16 +    @{const HOL.conj} $ negate_term t1 $ negate_term t2
   52.17    | negate_term (@{const Not} $ t) = t
   52.18    | negate_term t = @{const Not} $ t
   52.19  
    53.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 10:55:20 2010 +0200
    53.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 27 10:56:46 2010 +0200
    53.3 @@ -70,8 +70,8 @@
    53.4          do_quant bs AForall s T t'
    53.5        | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
    53.6          do_quant bs AExists s T t'
    53.7 -      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
    53.8 -      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
    53.9 +      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
   53.10 +      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
   53.11        | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
   53.12        | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   53.13          do_conn bs AIff t1 t2
   53.14 @@ -125,8 +125,8 @@
   53.15              t0 $ Abs (s, T, aux (T :: Ts) t')
   53.16            | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   53.17              aux Ts (t0 $ eta_expand Ts t1 1)
   53.18 -          | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   53.19 -          | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   53.20 +          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   53.21 +          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   53.22            | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   53.23            | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   53.24                $ t1 $ t2 =>
    54.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Fri Aug 27 10:55:20 2010 +0200
    54.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Fri Aug 27 10:56:46 2010 +0200
    54.3 @@ -79,11 +79,11 @@
    54.4    in capply c (uncurry cabs r) end;
    54.5  
    54.6  
    54.7 -local val c = mk_hol_const(@{const_name "op &"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    54.8 +local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    54.9  in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
   54.10  end;
   54.11  
   54.12 -local val c = mk_hol_const(@{const_name "op |"}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   54.13 +local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   54.14  in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
   54.15  end;
   54.16  
   54.17 @@ -129,8 +129,8 @@
   54.18  val dest_pair   = dest_binop @{const_name Pair}
   54.19  val dest_eq     = dest_binop @{const_name "op ="}
   54.20  val dest_imp    = dest_binop @{const_name HOL.implies}
   54.21 -val dest_conj   = dest_binop @{const_name "op &"}
   54.22 -val dest_disj   = dest_binop @{const_name "op |"}
   54.23 +val dest_conj   = dest_binop @{const_name HOL.conj}
   54.24 +val dest_disj   = dest_binop @{const_name HOL.disj}
   54.25  val dest_select = dest_binder @{const_name Eps}
   54.26  val dest_exists = dest_binder @{const_name Ex}
   54.27  val dest_forall = dest_binder @{const_name All}
    55.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Fri Aug 27 10:55:20 2010 +0200
    55.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Fri Aug 27 10:56:46 2010 +0200
    55.3 @@ -183,12 +183,12 @@
    55.4  
    55.5  
    55.6  fun mk_conj{conj1,conj2} =
    55.7 -   let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    55.8 +   let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    55.9     in list_comb(c,[conj1,conj2])
   55.10     end;
   55.11  
   55.12  fun mk_disj{disj1,disj2} =
   55.13 -   let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   55.14 +   let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
   55.15     in list_comb(c,[disj1,disj2])
   55.16     end;
   55.17  
   55.18 @@ -259,10 +259,10 @@
   55.19  fun dest_neg(Const(@{const_name Not},_) $ M) = M
   55.20    | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
   55.21  
   55.22 -fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
   55.23 +fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
   55.24    | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
   55.25  
   55.26 -fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
   55.27 +fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
   55.28    | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
   55.29  
   55.30  fun mk_pair{fst,snd} =
    56.1 --- a/src/HOL/Tools/cnf_funcs.ML	Fri Aug 27 10:55:20 2010 +0200
    56.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Fri Aug 27 10:56:46 2010 +0200
    56.3 @@ -95,8 +95,8 @@
    56.4  
    56.5  fun is_atom (Const (@{const_name False}, _))                                           = false
    56.6    | is_atom (Const (@{const_name True}, _))                                            = false
    56.7 -  | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
    56.8 -  | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
    56.9 +  | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _)                                    = false
   56.10 +  | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _)                                    = false
   56.11    | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _)                                  = false
   56.12    | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   56.13    | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   56.14 @@ -105,7 +105,7 @@
   56.15  fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
   56.16    | is_literal x                      = is_atom x;
   56.17  
   56.18 -fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
   56.19 +fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
   56.20    | is_clause x                           = is_literal x;
   56.21  
   56.22  (* ------------------------------------------------------------------------- *)
   56.23 @@ -184,14 +184,14 @@
   56.24  
   56.25  (* Theory.theory -> Term.term -> Thm.thm *)
   56.26  
   56.27 -fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
   56.28 +fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   56.29  	let
   56.30  		val thm1 = make_nnf_thm thy x
   56.31  		val thm2 = make_nnf_thm thy y
   56.32  	in
   56.33  		conj_cong OF [thm1, thm2]
   56.34  	end
   56.35 -  | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
   56.36 +  | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   56.37  	let
   56.38  		val thm1 = make_nnf_thm thy x
   56.39  		val thm2 = make_nnf_thm thy y
   56.40 @@ -218,14 +218,14 @@
   56.41  	make_nnf_not_false
   56.42    | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
   56.43  	make_nnf_not_true
   56.44 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
   56.45 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
   56.46  	let
   56.47  		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   56.48  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   56.49  	in
   56.50  		make_nnf_not_conj OF [thm1, thm2]
   56.51  	end
   56.52 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
   56.53 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
   56.54  	let
   56.55  		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   56.56  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
   56.57 @@ -276,7 +276,7 @@
   56.58  
   56.59  (* Theory.theory -> Term.term -> Thm.thm *)
   56.60  
   56.61 -fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
   56.62 +fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
   56.63  	let
   56.64  		val thm1 = simp_True_False_thm thy x
   56.65  		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   56.66 @@ -298,7 +298,7 @@
   56.67  					conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
   56.68  			end
   56.69  	end
   56.70 -  | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
   56.71 +  | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
   56.72  	let
   56.73  		val thm1 = simp_True_False_thm thy x
   56.74  		val x'   = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   56.75 @@ -334,24 +334,24 @@
   56.76  fun make_cnf_thm thy t =
   56.77  let
   56.78  	(* Term.term -> Thm.thm *)
   56.79 -	fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
   56.80 +	fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
   56.81  		let
   56.82  			val thm1 = make_cnf_thm_from_nnf x
   56.83  			val thm2 = make_cnf_thm_from_nnf y
   56.84  		in
   56.85  			conj_cong OF [thm1, thm2]
   56.86  		end
   56.87 -	  | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
   56.88 +	  | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
   56.89  		let
   56.90  			(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
   56.91 -			fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
   56.92 +			fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
   56.93  				let
   56.94  					val thm1 = make_cnf_disj_thm x1 y'
   56.95  					val thm2 = make_cnf_disj_thm x2 y'
   56.96  				in
   56.97  					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
   56.98  				end
   56.99 -			  | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
  56.100 +			  | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
  56.101  				let
  56.102  					val thm1 = make_cnf_disj_thm x' y1
  56.103  					val thm2 = make_cnf_disj_thm x' y2
  56.104 @@ -403,27 +403,27 @@
  56.105  	val var_id = Unsynchronized.ref 0  (* properly initialized below *)
  56.106  	fun new_free () =
  56.107  		Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
  56.108 -	fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
  56.109 +	fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
  56.110  		let
  56.111  			val thm1 = make_cnfx_thm_from_nnf x
  56.112  			val thm2 = make_cnfx_thm_from_nnf y
  56.113  		in
  56.114  			conj_cong OF [thm1, thm2]
  56.115  		end
  56.116 -	  | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
  56.117 +	  | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
  56.118  		if is_clause x andalso is_clause y then
  56.119  			inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
  56.120  		else if is_literal y orelse is_literal x then let
  56.121  			(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
  56.122  			(* almost in CNF, and x' or y' is a literal                      *)
  56.123 -			fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
  56.124 +			fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
  56.125  				let
  56.126  					val thm1 = make_cnfx_disj_thm x1 y'
  56.127  					val thm2 = make_cnfx_disj_thm x2 y'
  56.128  				in
  56.129  					make_cnf_disj_conj_l OF [thm1, thm2]  (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
  56.130  				end
  56.131 -			  | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
  56.132 +			  | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
  56.133  				let
  56.134  					val thm1 = make_cnfx_disj_thm x' y1
  56.135  					val thm2 = make_cnfx_disj_thm x' y2
    57.1 --- a/src/HOL/Tools/groebner.ML	Fri Aug 27 10:55:20 2010 +0200
    57.2 +++ b/src/HOL/Tools/groebner.ML	Fri Aug 27 10:56:46 2010 +0200
    57.3 @@ -395,7 +395,7 @@
    57.4  
    57.5  fun refute_disj rfn tm =
    57.6   case term_of tm of
    57.7 -  Const(@{const_name "op |"},_)$l$r =>
    57.8 +  Const(@{const_name HOL.disj},_)$l$r =>
    57.9     compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE))
   57.10    | _ => rfn tm ;
   57.11  
   57.12 @@ -454,7 +454,7 @@
   57.13  val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   57.14  
   57.15  val cTrp = @{cterm "Trueprop"};
   57.16 -val cConj = @{cterm "op &"};
   57.17 +val cConj = @{cterm HOL.conj};
   57.18  val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
   57.19  val assume_Trueprop = mk_comb cTrp #> assume;
   57.20  val list_mk_conj = list_mk_binop cConj;
   57.21 @@ -479,22 +479,22 @@
   57.22    (* FIXME : copied from cqe.ML -- complex QE*)
   57.23  fun conjuncts ct =
   57.24   case term_of ct of
   57.25 -  @{term "op &"}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
   57.26 +  @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
   57.27  | _ => [ct];
   57.28  
   57.29  fun fold1 f = foldr1 (uncurry f);
   57.30  
   57.31 -val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm "op &"} c) c') ;
   57.32 +val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
   57.33  
   57.34  fun mk_conj_tab th = 
   57.35   let fun h acc th = 
   57.36     case prop_of th of
   57.37 -   @{term "Trueprop"}$(@{term "op &"}$p$q) => 
   57.38 +   @{term "Trueprop"}$(@{term HOL.conj}$p$q) => 
   57.39       h (h acc (th RS conjunct2)) (th RS conjunct1)
   57.40    | @{term "Trueprop"}$p => (p,th)::acc
   57.41  in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
   57.42  
   57.43 -fun is_conj (@{term "op &"}$_$_) = true
   57.44 +fun is_conj (@{term HOL.conj}$_$_) = true
   57.45    | is_conj _ = false;
   57.46  
   57.47  fun prove_conj tab cjs = 
   57.48 @@ -852,14 +852,14 @@
   57.49   fun unwind_polys_conv tm =
   57.50   let 
   57.51    val (vars,bod) = strip_exists tm
   57.52 -  val cjs = striplist (dest_binary @{cterm "op &"}) bod
   57.53 +  val cjs = striplist (dest_binary @{cterm HOL.conj}) bod
   57.54    val th1 = (the (get_first (try (isolate_variable vars)) cjs) 
   57.55               handle Option => raise CTERM ("unwind_polys_conv",[tm]))
   57.56    val eq = Thm.lhs_of th1
   57.57 -  val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
   57.58 +  val bod' = list_mk_binop @{cterm HOL.conj} (eq::(remove op aconvc eq cjs))
   57.59    val th2 = conj_ac_rule (mk_eq bod bod')
   57.60    val th3 = transitive th2 
   57.61 -         (Drule.binop_cong_rule @{cterm "op &"} th1 
   57.62 +         (Drule.binop_cong_rule @{cterm HOL.conj} th1 
   57.63                  (reflexive (Thm.dest_arg (Thm.rhs_of th2))))
   57.64    val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
   57.65    val vars' = (remove op aconvc v vars) @ [v]
   57.66 @@ -929,8 +929,8 @@
   57.67    | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
   57.68    | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
   57.69    | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
   57.70 -  | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   57.71 -  | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
   57.72 +  | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
   57.73 +  | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
   57.74    | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   57.75    | @{term "op ==>"} $_$_ => find_args bounds tm
   57.76    | Const("op ==",_)$_$_ => find_args bounds tm
    58.1 --- a/src/HOL/Tools/hologic.ML	Fri Aug 27 10:55:20 2010 +0200
    58.2 +++ b/src/HOL/Tools/hologic.ML	Fri Aug 27 10:56:46 2010 +0200
    58.3 @@ -208,8 +208,8 @@
    58.4    let val (th1, th2) = conj_elim th
    58.5    in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
    58.6  
    58.7 -val conj = @{term "op &"}
    58.8 -and disj = @{term "op |"}
    58.9 +val conj = @{term HOL.conj}
   58.10 +and disj = @{term HOL.disj}
   58.11  and imp = @{term implies}
   58.12  and Not = @{term Not};
   58.13  
   58.14 @@ -218,14 +218,14 @@
   58.15  and mk_imp (t1, t2) = imp $ t1 $ t2
   58.16  and mk_not t = Not $ t;
   58.17  
   58.18 -fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
   58.19 +fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
   58.20    | dest_conj t = [t];
   58.21  
   58.22 -fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
   58.23 +fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
   58.24    | dest_disj t = [t];
   58.25  
   58.26  (*Like dest_disj, but flattens disjunctions however nested*)
   58.27 -fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
   58.28 +fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
   58.29    | disjuncts_aux t disjs = t::disjs;
   58.30  
   58.31  fun disjuncts t = disjuncts_aux t [];
    59.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Aug 27 10:55:20 2010 +0200
    59.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Aug 27 10:56:46 2010 +0200
    59.3 @@ -74,9 +74,9 @@
    59.4          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
    59.5            (p (fold (Logic.all o Var) vs t) f)
    59.6          end;
    59.7 -      fun mkop @{const_name "op &"} T x =
    59.8 +      fun mkop @{const_name HOL.conj} T x =
    59.9              SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   59.10 -        | mkop @{const_name "op |"} T x =
   59.11 +        | mkop @{const_name HOL.disj} T x =
   59.12              SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   59.13          | mkop _ _ _ = NONE;
   59.14        fun mk_collect p T t =
    60.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Aug 27 10:55:20 2010 +0200
    60.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Aug 27 10:56:46 2010 +0200
    60.3 @@ -46,7 +46,7 @@
    60.4  val mk_Trueprop = HOLogic.mk_Trueprop;
    60.5  
    60.6  fun atomize thm = case Thm.prop_of thm of
    60.7 -    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
    60.8 +    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
    60.9      atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
   60.10    | _ => [thm];
   60.11  
    61.1 --- a/src/HOL/Tools/meson.ML	Fri Aug 27 10:55:20 2010 +0200
    61.2 +++ b/src/HOL/Tools/meson.ML	Fri Aug 27 10:56:46 2010 +0200
    61.3 @@ -151,8 +151,8 @@
    61.4    let fun has (Const(a,_)) = false
    61.5          | has (Const(@{const_name Trueprop},_) $ p) = has p
    61.6          | has (Const(@{const_name Not},_) $ p) = has p
    61.7 -        | has (Const(@{const_name "op |"},_) $ p $ q) = member (op =) bs @{const_name "op |"} orelse has p orelse has q
    61.8 -        | has (Const(@{const_name "op &"},_) $ p $ q) = member (op =) bs @{const_name "op &"} orelse has p orelse has q
    61.9 +        | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q
   61.10 +        | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q
   61.11          | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p
   61.12          | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p
   61.13          | has _ = false
   61.14 @@ -162,7 +162,7 @@
   61.15  (**** Clause handling ****)
   61.16  
   61.17  fun literals (Const(@{const_name Trueprop},_) $ P) = literals P
   61.18 -  | literals (Const(@{const_name "op |"},_) $ P $ Q) = literals P @ literals Q
   61.19 +  | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q
   61.20    | literals (Const(@{const_name Not},_) $ P) = [(false,P)]
   61.21    | literals P = [(true,P)];
   61.22  
   61.23 @@ -172,7 +172,7 @@
   61.24  
   61.25  (*** Tautology Checking ***)
   61.26  
   61.27 -fun signed_lits_aux (Const (@{const_name "op |"}, _) $ P $ Q) (poslits, neglits) =
   61.28 +fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) =
   61.29        signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
   61.30    | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
   61.31    | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
   61.32 @@ -208,16 +208,16 @@
   61.33  fun refl_clause_aux 0 th = th
   61.34    | refl_clause_aux n th =
   61.35         case HOLogic.dest_Trueprop (concl_of th) of
   61.36 -          (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _) =>
   61.37 +          (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
   61.38              refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
   61.39 -        | (Const (@{const_name "op |"}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
   61.40 +        | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ t $ u)) $ _) =>
   61.41              if eliminable(t,u)
   61.42              then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
   61.43              else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
   61.44 -        | (Const (@{const_name "op |"}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
   61.45 +        | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
   61.46          | _ => (*not a disjunction*) th;
   61.47  
   61.48 -fun notequal_lits_count (Const (@{const_name "op |"}, _) $ P $ Q) =
   61.49 +fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) =
   61.50        notequal_lits_count P + notequal_lits_count Q
   61.51    | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name "op ="},_) $ _ $ _)) = 1
   61.52    | notequal_lits_count _ = 0;
   61.53 @@ -268,10 +268,10 @@
   61.54    (*Estimate the number of clauses in order to detect infeasible theorems*)
   61.55    fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t
   61.56      | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t
   61.57 -    | signed_nclauses b (Const(@{const_name "op &"},_) $ t $ u) =
   61.58 +    | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) =
   61.59          if b then sum (signed_nclauses b t) (signed_nclauses b u)
   61.60               else prod (signed_nclauses b t) (signed_nclauses b u)
   61.61 -    | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
   61.62 +    | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) =
   61.63          if b then prod (signed_nclauses b t) (signed_nclauses b u)
   61.64               else sum (signed_nclauses b t) (signed_nclauses b u)
   61.65      | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
   61.66 @@ -330,10 +330,10 @@
   61.67    let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
   61.68        fun cnf_aux (th,ths) =
   61.69          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   61.70 -        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name "op &"}] (prop_of th))
   61.71 +        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
   61.72          then nodups ctxt th :: ths (*no work to do, terminate*)
   61.73          else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   61.74 -            Const (@{const_name "op &"}, _) => (*conjunction*)
   61.75 +            Const (@{const_name HOL.conj}, _) => (*conjunction*)
   61.76                  cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
   61.77            | Const (@{const_name All}, _) => (*universal quantifier*)
   61.78                  let val (th',ctxt') = freeze_spec th (!ctxtr)
   61.79 @@ -341,7 +341,7 @@
   61.80            | Const (@{const_name Ex}, _) =>
   61.81                (*existential quantifier: Insert Skolem functions*)
   61.82                cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
   61.83 -          | Const (@{const_name "op |"}, _) =>
   61.84 +          | Const (@{const_name HOL.disj}, _) =>
   61.85                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
   61.86                  all combinations of converting P, Q to CNF.*)
   61.87                let val tac =
   61.88 @@ -365,7 +365,7 @@
   61.89  (**** Generation of contrapositives ****)
   61.90  
   61.91  fun is_left (Const (@{const_name Trueprop}, _) $
   61.92 -               (Const (@{const_name "op |"}, _) $ (Const (@{const_name "op |"}, _) $ _ $ _) $ _)) = true
   61.93 +               (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true
   61.94    | is_left _ = false;
   61.95  
   61.96  (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   61.97 @@ -400,7 +400,7 @@
   61.98  (*Is the string the name of a connective? Really only | and Not can remain,
   61.99    since this code expects to be called on a clause form.*)
  61.100  val is_conn = member (op =)
  61.101 -    [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
  61.102 +    [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
  61.103       @{const_name HOL.implies}, @{const_name Not},
  61.104       @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
  61.105  
  61.106 @@ -429,7 +429,7 @@
  61.107  
  61.108  fun rigid t = not (is_Var (head_of t));
  61.109  
  61.110 -fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name "op |"}, _) $ t $ _)) = rigid t
  61.111 +fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t
  61.112    | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t
  61.113    | ok4horn _ = false;
  61.114  
    62.1 --- a/src/HOL/Tools/prop_logic.ML	Fri Aug 27 10:55:20 2010 +0200
    62.2 +++ b/src/HOL/Tools/prop_logic.ML	Fri Aug 27 10:56:46 2010 +0200
    62.3 @@ -397,14 +397,14 @@
    62.4  			(False, table)
    62.5  		  | aux (Const (@{const_name Not}, _) $ x)      table =
    62.6  			apfst Not (aux x table)
    62.7 -		  | aux (Const (@{const_name "op |"}, _) $ x $ y) table =
    62.8 +		  | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
    62.9  			let
   62.10  				val (fm1, table1) = aux x table
   62.11  				val (fm2, table2) = aux y table1
   62.12  			in
   62.13  				(Or (fm1, fm2), table2)
   62.14  			end
   62.15 -		  | aux (Const (@{const_name "op &"}, _) $ x $ y) table =
   62.16 +		  | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
   62.17  			let
   62.18  				val (fm1, table1) = aux x table
   62.19  				val (fm2, table2) = aux y table1
    63.1 --- a/src/HOL/Tools/refute.ML	Fri Aug 27 10:55:20 2010 +0200
    63.2 +++ b/src/HOL/Tools/refute.ML	Fri Aug 27 10:56:46 2010 +0200
    63.3 @@ -648,8 +648,8 @@
    63.4        | Const (@{const_name All}, _) => t
    63.5        | Const (@{const_name Ex}, _) => t
    63.6        | Const (@{const_name "op ="}, _) => t
    63.7 -      | Const (@{const_name "op &"}, _) => t
    63.8 -      | Const (@{const_name "op |"}, _) => t
    63.9 +      | Const (@{const_name HOL.conj}, _) => t
   63.10 +      | Const (@{const_name HOL.disj}, _) => t
   63.11        | Const (@{const_name HOL.implies}, _) => t
   63.12        (* sets *)
   63.13        | Const (@{const_name Collect}, _) => t
   63.14 @@ -824,8 +824,8 @@
   63.15        | Const (@{const_name All}, T) => collect_type_axioms T axs
   63.16        | Const (@{const_name Ex}, T) => collect_type_axioms T axs
   63.17        | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
   63.18 -      | Const (@{const_name "op &"}, _) => axs
   63.19 -      | Const (@{const_name "op |"}, _) => axs
   63.20 +      | Const (@{const_name HOL.conj}, _) => axs
   63.21 +      | Const (@{const_name HOL.disj}, _) => axs
   63.22        | Const (@{const_name HOL.implies}, _) => axs
   63.23        (* sets *)
   63.24        | Const (@{const_name Collect}, T) => collect_type_axioms T axs
   63.25 @@ -1861,7 +1861,7 @@
   63.26        SOME (interpret thy model args (eta_expand t 1))
   63.27      | Const (@{const_name "op ="}, _) =>
   63.28        SOME (interpret thy model args (eta_expand t 2))
   63.29 -    | Const (@{const_name "op &"}, _) $ t1 $ t2 =>
   63.30 +    | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
   63.31        (* 3-valued logic *)
   63.32        let
   63.33          val (i1, m1, a1) = interpret thy model args t1
   63.34 @@ -1871,14 +1871,14 @@
   63.35        in
   63.36          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   63.37        end
   63.38 -    | Const (@{const_name "op &"}, _) $ t1 =>
   63.39 +    | Const (@{const_name HOL.conj}, _) $ t1 =>
   63.40        SOME (interpret thy model args (eta_expand t 1))
   63.41 -    | Const (@{const_name "op &"}, _) =>
   63.42 +    | Const (@{const_name HOL.conj}, _) =>
   63.43        SOME (interpret thy model args (eta_expand t 2))
   63.44        (* this would make "undef" propagate, even for formulae like *)
   63.45        (* "False & undef":                                          *)
   63.46        (* SOME (Node [Node [TT, FF], Node [FF, FF]], model, args) *)
   63.47 -    | Const (@{const_name "op |"}, _) $ t1 $ t2 =>
   63.48 +    | Const (@{const_name HOL.disj}, _) $ t1 $ t2 =>
   63.49        (* 3-valued logic *)
   63.50        let
   63.51          val (i1, m1, a1) = interpret thy model args t1
   63.52 @@ -1888,9 +1888,9 @@
   63.53        in
   63.54          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   63.55        end
   63.56 -    | Const (@{const_name "op |"}, _) $ t1 =>
   63.57 +    | Const (@{const_name HOL.disj}, _) $ t1 =>
   63.58        SOME (interpret thy model args (eta_expand t 1))
   63.59 -    | Const (@{const_name "op |"}, _) =>
   63.60 +    | Const (@{const_name HOL.disj}, _) =>
   63.61        SOME (interpret thy model args (eta_expand t 2))
   63.62        (* this would make "undef" propagate, even for formulae like *)
   63.63        (* "True | undef":                                           *)
    64.1 --- a/src/HOL/Tools/simpdata.ML	Fri Aug 27 10:55:20 2010 +0200
    64.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Aug 27 10:56:46 2010 +0200
    64.3 @@ -12,7 +12,7 @@
    64.4    (*abstract syntax*)
    64.5    fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
    64.6      | dest_eq _ = NONE;
    64.7 -  fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
    64.8 +  fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
    64.9      | dest_conj _ = NONE;
   64.10    fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
   64.11      | dest_imp _ = NONE;
   64.12 @@ -160,7 +160,7 @@
   64.13  
   64.14  val mksimps_pairs =
   64.15   [(@{const_name HOL.implies}, [@{thm mp}]),
   64.16 -  (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
   64.17 +  (@{const_name HOL.conj}, [@{thm conjunct1}, @{thm conjunct2}]),
   64.18    (@{const_name All}, [@{thm spec}]),
   64.19    (@{const_name True}, []),
   64.20    (@{const_name False}, []),
    65.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Aug 27 10:55:20 2010 +0200
    65.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Aug 27 10:56:46 2010 +0200
    65.3 @@ -88,8 +88,8 @@
    65.4              else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    65.5              else replace (c $ x $ y)   (*non-numeric comparison*)
    65.6      (*abstraction of a formula*)
    65.7 -    and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    65.8 -      | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    65.9 +    and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
   65.10 +      | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
   65.11        | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
   65.12        | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
   65.13        | fm ((c as Const(@{const_name True}, _))) = c
    66.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Aug 27 10:55:20 2010 +0200
    66.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Aug 27 10:56:46 2010 +0200
    66.3 @@ -89,8 +89,8 @@
    66.4     let fun tag t =
    66.5           let val (c,ts) = strip_comb t
    66.6           in  case c of
    66.7 -             Const(@{const_name "op &"}, _)   => apply c (map tag ts)
    66.8 -           | Const(@{const_name "op |"}, _)   => apply c (map tag ts)
    66.9 +             Const(@{const_name HOL.conj}, _)   => apply c (map tag ts)
   66.10 +           | Const(@{const_name HOL.disj}, _)   => apply c (map tag ts)
   66.11             | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
   66.12             | Const(@{const_name Not}, _)    => apply c (map tag ts)
   66.13             | Const(@{const_name True}, _)   => (c, false)
   66.14 @@ -183,9 +183,9 @@
   66.15        | tm t = Int (lit t)
   66.16                 handle Match => var (t,[])
   66.17      (*translation of a formula*)
   66.18 -    and fm pos (Const(@{const_name "op &"}, _) $ p $ q) =
   66.19 +    and fm pos (Const(@{const_name HOL.conj}, _) $ p $ q) =
   66.20              Buildin("AND", [fm pos p, fm pos q])
   66.21 -      | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
   66.22 +      | fm pos (Const(@{const_name HOL.disj}, _) $ p $ q) =
   66.23              Buildin("OR", [fm pos p, fm pos q])
   66.24        | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
   66.25              Buildin("=>", [fm (not pos) p, fm pos q])
    67.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Fri Aug 27 10:55:20 2010 +0200
    67.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Fri Aug 27 10:56:46 2010 +0200
    67.3 @@ -121,7 +121,7 @@
    67.4        val r_inst = read_instantiate ctxt;
    67.5        fun at thm =
    67.6            case concl_of thm of
    67.7 -            _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    67.8 +            _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    67.9            | _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec))
   67.10            | _                             => [thm];
   67.11      in map zero_var_indexes (at thm) end;
    68.1 --- a/src/Tools/Code/code_thingol.ML	Fri Aug 27 10:55:20 2010 +0200
    68.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Aug 27 10:56:46 2010 +0200
    68.3 @@ -271,9 +271,6 @@
    68.4         of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
    68.5          | NONE => Codegen.thyname_of_const thy c);
    68.6    fun purify_base "==>" = "follows"
    68.7 -    | purify_base "op &" = "and"
    68.8 -    | purify_base "op |" = "or"
    68.9 -    | purify_base "op -->" = "implies"
   68.10      | purify_base "op =" = "eq"
   68.11      | purify_base s = Name.desymbolize false s;
   68.12    fun namify thy get_basename get_thyname name =