more antiquotations;
authorwenzelm
Fri Dec 02 14:54:25 2011 +0100 (2011-12-02)
changeset 45740132a3e1c0fe5
parent 45739 b545ea8bc731
child 45741 088256c289e7
more antiquotations;
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/ATP/atp_reconstruct.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/sat_funcs.ML
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Dec 02 14:37:25 2011 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Dec 02 14:54:25 2011 +0100
     1.3 @@ -1943,8 +1943,8 @@
     1.4        term_of_num vs (@{code C} i) $ term_of_num vs t2
     1.5    | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
     1.6  
     1.7 -fun term_of_fm ps vs @{code T} = HOLogic.true_const 
     1.8 -  | term_of_fm ps vs @{code F} = HOLogic.false_const
     1.9 +fun term_of_fm ps vs @{code T} = @{term True} 
    1.10 +  | term_of_fm ps vs @{code F} = @{term False}
    1.11    | term_of_fm ps vs (@{code Lt} t) =
    1.12        @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
    1.13    | term_of_fm ps vs (@{code Le} t) =
     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Dec 02 14:37:25 2011 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Dec 02 14:54:25 2011 +0100
     2.3 @@ -1976,8 +1976,8 @@
     2.4        term_of_num vs (@{code C} i) $ term_of_num vs t2
     2.5    | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
     2.6  
     2.7 -fun term_of_fm vs @{code T} = HOLogic.true_const 
     2.8 -  | term_of_fm vs @{code F} = HOLogic.false_const
     2.9 +fun term_of_fm vs @{code T} = @{term True} 
    2.10 +  | term_of_fm vs @{code F} = @{term False}
    2.11    | term_of_fm vs (@{code Lt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $
    2.12        term_of_num vs t $ @{term "0::real"}
    2.13    | term_of_fm vs (@{code Le} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $
     3.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Dec 02 14:37:25 2011 +0100
     3.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Dec 02 14:54:25 2011 +0100
     3.3 @@ -5602,8 +5602,8 @@
     3.4    | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
     3.5    | term_of_num vs (@{code CF} (c, t, s)) = term_of_num vs (@{code Add} (@{code Mul} (c, @{code Floor} t), s));
     3.6  
     3.7 -fun term_of_fm vs @{code T} = HOLogic.true_const 
     3.8 -  | term_of_fm vs @{code F} = HOLogic.false_const
     3.9 +fun term_of_fm vs @{code T} = @{term True} 
    3.10 +  | term_of_fm vs @{code F} = @{term False}
    3.11    | term_of_fm vs (@{code Lt} t) =
    3.12        @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::real"}
    3.13    | term_of_fm vs (@{code Le} t) =
     4.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 14:37:25 2011 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Dec 02 14:54:25 2011 +0100
     4.3 @@ -1025,7 +1025,7 @@
     4.4             Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
     4.5               (HOLogic.mk_Trueprop (HOLogic.mk_eq
     4.6                 (fresh c,
     4.7 -                if null dts then HOLogic.true_const
     4.8 +                if null dts then @{term True}
     4.9                  else foldr1 HOLogic.mk_conj (map fresh args2)))))
    4.10               (fn _ =>
    4.11                 simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
     5.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 02 14:37:25 2011 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 02 14:54:25 2011 +0100
     5.3 @@ -308,7 +308,7 @@
     5.4        curry (List.take o swap) (length fvars) |> map cert;
     5.5      val invs' = (case invs of
     5.6          NONE => map (fn (i, _) =>
     5.7 -          Abs ("x", fastype_of (snd (nth defs' i)), HOLogic.true_const)) descr
     5.8 +          Abs ("x", fastype_of (snd (nth defs' i)), @{term True})) descr
     5.9        | SOME invs' => map (prep_term lthy') invs');
    5.10      val inst = (map cert fvars ~~ cfs) @
    5.11        (map (cert o Var) pvars ~~ map cert invs') @
     6.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 02 14:37:25 2011 +0100
     6.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 02 14:54:25 2011 +0100
     6.3 @@ -1003,8 +1003,8 @@
     6.4  
     6.5      val (((defs', vars''), ivars), (ids, thy')) =
     6.6        ((Symtab.empty |>
     6.7 -        Symtab.update ("false", (HOLogic.false_const, booleanN)) |>
     6.8 -        Symtab.update ("true", (HOLogic.true_const, booleanN)),
     6.9 +        Symtab.update ("false", (@{term False}, booleanN)) |>
    6.10 +        Symtab.update ("true", (@{term True}, booleanN)),
    6.11          Name.context),
    6.12         thy |> Sign.add_path (Long_Name.base_name ident)) |>
    6.13        fold (add_type_def prfx) (items types) |>
     7.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Dec 02 14:37:25 2011 +0100
     7.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Dec 02 14:54:25 2011 +0100
     7.3 @@ -29,6 +29,7 @@
     7.4  datatype direction = Left | Right;
     7.5  
     7.6  fun treeT T = Type (@{type_name tree}, [T]);
     7.7 +
     7.8  fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T)
     7.9    | mk_tree' e T n xs =
    7.10       let
    7.11 @@ -38,7 +39,7 @@
    7.12         val r = mk_tree' e T (n-(m+1)) xsr;
    7.13       in
    7.14         Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $
    7.15 -         l $ e x $ HOLogic.false_const $ r
    7.16 +         l $ e x $ @{term False} $ r
    7.17       end
    7.18  
    7.19  fun mk_tree e T xs = mk_tree' e T (length xs) xs;
     8.1 --- a/src/HOL/Statespace/state_fun.ML	Fri Dec 02 14:37:25 2011 +0100
     8.2 +++ b/src/HOL/Statespace/state_fun.ML	Fri Dec 02 14:54:25 2011 +0100
     8.3 @@ -309,7 +309,7 @@
     8.4                val (eq, eT, nT, swap) = mkeq (dest_sel_eq t) 0;
     8.5                val prop =
     8.6                  list_all ([("n", nT), ("x", eT)],
     8.7 -                  Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
     8.8 +                  Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
     8.9                val thm = Drule.export_without_context (prove prop);
    8.10                val thm' = if swap then swap_ex_eq OF [thm] else thm
    8.11              in SOME thm' end handle TERM _ => NONE)
     9.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Dec 02 14:37:25 2011 +0100
     9.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Dec 02 14:54:25 2011 +0100
     9.3 @@ -586,7 +586,7 @@
     9.4  
     9.5  (* No "real" literals means only type information (tfree_tcs, clsrel, or
     9.6     clsarity). *)
     9.7 -val is_only_type_information = curry (op aconv) HOLogic.true_const
     9.8 +val is_only_type_information = curry (op aconv) @{term True}
     9.9  
    9.10  fun replace_one_dependency (old, new) dep =
    9.11    if is_same_atp_step dep old then new else [dep]
    10.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 14:37:25 2011 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 14:54:25 2011 +0100
    10.3 @@ -478,7 +478,7 @@
    10.4        let val isoT = T --> Univ_elT in
    10.5          HOLogic.imp $
    10.6            (Const (set_name, UnivT') $ Datatype_Aux.mk_Free "x" Univ_elT i) $
    10.7 -            (if i < length newTs then HOLogic.true_const
    10.8 +            (if i < length newTs then @{term True}
    10.9               else HOLogic.mk_mem (Datatype_Aux.mk_Free "x" Univ_elT i,
   10.10                 Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
   10.11                   Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
    11.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 02 14:37:25 2011 +0100
    11.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 02 14:54:25 2011 +0100
    11.3 @@ -68,8 +68,8 @@
    11.4        Datatype_Data.the_info thy tyco;
    11.5      val ty = Type (tyco, map TFree vs);
    11.6      fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT) $ t1 $ t2;
    11.7 -    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
    11.8 -    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
    11.9 +    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term True});
   11.10 +    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term False});
   11.11      val triv_injects =
   11.12        map_filter
   11.13          (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
    12.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Dec 02 14:37:25 2011 +0100
    12.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Dec 02 14:54:25 2011 +0100
    12.3 @@ -79,7 +79,7 @@
    12.4        (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
    12.5           Solved thm2 => LessEq (thm2, thm)
    12.6         | Stuck thm2 =>
    12.7 -         if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
    12.8 +         if prems_of thm2 = [HOLogic.Trueprop $ @{term False}] then False thm2
    12.9           else None (thm2, thm)
   12.10         | _ => raise Match) (* FIXME *)
   12.11      | _ => raise Match
    13.1 --- a/src/HOL/Tools/Function/size.ML	Fri Dec 02 14:37:25 2011 +0100
    13.2 +++ b/src/HOL/Tools/Function/size.ML	Fri Dec 02 14:54:25 2011 +0100
    13.3 @@ -160,7 +160,7 @@
    13.4      fun prove_unfolded_size_eqs size_ofp fs =
    13.5        if null recTs2 then []
    13.6        else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs []
    13.7 -        (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l HOLogic.true_const @
    13.8 +        (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @
    13.9             map (mk_unfolded_size_eq (AList.lookup op =
   13.10                 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
   13.11               (xs ~~ recTs2 ~~ rec_combs2))))
    14.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Dec 02 14:37:25 2011 +0100
    14.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Dec 02 14:54:25 2011 +0100
    14.3 @@ -182,7 +182,7 @@
    14.4         (case try @{const_name Orderings.less_eq} of
    14.5            Solved thm2 => LessEq (thm2, thm)
    14.6          | Stuck thm2 =>
    14.7 -          if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
    14.8 +          if prems_of thm2 = [HOLogic.Trueprop $ @{term False}]
    14.9            then False thm2 else None (thm2, thm)
   14.10          | _ => raise Match) (* FIXME *)
   14.11       | _ => raise Match
   14.12 @@ -260,7 +260,7 @@
   14.13      val pT = HOLogic.mk_prodT (T, T)
   14.14      val n = length qs
   14.15      val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
   14.16 -    val conds' = if null conds then [HOLogic.true_const] else conds
   14.17 +    val conds' = if null conds then [@{term True}] else conds
   14.18    in
   14.19      HOLogic.Collect_const pT $
   14.20      Abs ("uu_", pT,
    15.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Dec 02 14:37:25 2011 +0100
    15.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Dec 02 14:54:25 2011 +0100
    15.3 @@ -231,7 +231,7 @@
    15.4    let val (poslits,neglits) = signed_lits th
    15.5    in  exists taut_poslit poslits
    15.6        orelse
    15.7 -      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
    15.8 +      exists (member (op aconv) neglits) (@{term False} :: poslits)
    15.9    end
   15.10    handle TERM _ => false;       (*probably dest_Trueprop on a weird theorem*)
   15.11  
    16.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 02 14:37:25 2011 +0100
    16.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 02 14:54:25 2011 +0100
    16.3 @@ -35,8 +35,8 @@
    16.4  
    16.5  (**** Transformation of Elimination Rules into First-Order Formulas****)
    16.6  
    16.7 -val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
    16.8 -val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
    16.9 +val cfalse = cterm_of @{theory HOL} @{term False};
   16.10 +val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop @{term False});
   16.11  
   16.12  (* Converts an elim-rule into an equivalent theorem that does not have the
   16.13     predicate variable. Leaves other theorems unchanged. We simply instantiate
    17.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Dec 02 14:37:25 2011 +0100
    17.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Dec 02 14:54:25 2011 +0100
    17.3 @@ -653,8 +653,8 @@
    17.4    | term_of_num vs (Proc.Cn (n, i, t')) =
    17.5        term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
    17.6  
    17.7 -fun term_of_fm ps vs Proc.T = HOLogic.true_const
    17.8 -  | term_of_fm ps vs Proc.F = HOLogic.false_const
    17.9 +fun term_of_fm ps vs Proc.T = @{term True}
   17.10 +  | term_of_fm ps vs Proc.F = @{term False}
   17.11    | term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   17.12    | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
   17.13    | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
    18.1 --- a/src/HOL/Tools/cnf_funcs.ML	Fri Dec 02 14:37:25 2011 +0100
    18.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Fri Dec 02 14:54:25 2011 +0100
    18.3 @@ -294,18 +294,18 @@
    18.4          val thm1 = simp_True_False_thm thy x
    18.5          val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
    18.6        in
    18.7 -        if x' = HOLogic.false_const then
    18.8 +        if x' = @{term False} then
    18.9            simp_TF_conj_False_l OF [thm1]  (* (x & y) = False *)
   18.10          else
   18.11            let
   18.12              val thm2 = simp_True_False_thm thy y
   18.13              val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   18.14            in
   18.15 -            if x' = HOLogic.true_const then
   18.16 +            if x' = @{term True} then
   18.17                simp_TF_conj_True_l OF [thm1, thm2]  (* (x & y) = y' *)
   18.18 -            else if y' = HOLogic.false_const then
   18.19 +            else if y' = @{term False} then
   18.20                simp_TF_conj_False_r OF [thm2]  (* (x & y) = False *)
   18.21 -            else if y' = HOLogic.true_const then
   18.22 +            else if y' = @{term True} then
   18.23                simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
   18.24              else
   18.25                conj_cong OF [thm1, thm2]  (* (x & y) = (x' & y') *)
   18.26 @@ -316,18 +316,18 @@
   18.27          val thm1 = simp_True_False_thm thy x
   18.28          val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
   18.29        in
   18.30 -        if x' = HOLogic.true_const then
   18.31 +        if x' = @{term True} then
   18.32            simp_TF_disj_True_l OF [thm1]  (* (x | y) = True *)
   18.33          else
   18.34            let
   18.35              val thm2 = simp_True_False_thm thy y
   18.36              val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
   18.37            in
   18.38 -            if x' = HOLogic.false_const then
   18.39 +            if x' = @{term False} then
   18.40                simp_TF_disj_False_l OF [thm1, thm2]  (* (x | y) = y' *)
   18.41 -            else if y' = HOLogic.true_const then
   18.42 +            else if y' = @{term True} then
   18.43                simp_TF_disj_True_r OF [thm2]  (* (x | y) = True *)
   18.44 -            else if y' = HOLogic.false_const then
   18.45 +            else if y' = @{term False} then
   18.46                simp_TF_disj_False_r OF [thm1, thm2]  (* (x | y) = x' *)
   18.47              else
   18.48                disj_cong OF [thm1, thm2]  (* (x | y) = (x' | y') *)
    19.1 --- a/src/HOL/Tools/hologic.ML	Fri Dec 02 14:37:25 2011 +0100
    19.2 +++ b/src/HOL/Tools/hologic.ML	Fri Dec 02 14:54:25 2011 +0100
    19.3 @@ -15,8 +15,6 @@
    19.4    val Trueprop: term
    19.5    val mk_Trueprop: term -> term
    19.6    val dest_Trueprop: term -> term
    19.7 -  val true_const: term
    19.8 -  val false_const: term
    19.9    val mk_induct_forall: typ -> term
   19.10    val mk_setT: typ -> typ
   19.11    val dest_setT: typ -> typ
   19.12 @@ -162,9 +160,6 @@
   19.13  val boolN = "HOL.bool";
   19.14  val boolT = Type (boolN, []);
   19.15  
   19.16 -val true_const =  Const ("HOL.True", boolT);
   19.17 -val false_const = Const ("HOL.False", boolT);
   19.18 -
   19.19  fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
   19.20  
   19.21  fun mk_setT T = T --> boolT;
    20.1 --- a/src/HOL/Tools/inductive.ML	Fri Dec 02 14:37:25 2011 +0100
    20.2 +++ b/src/HOL/Tools/inductive.ML	Fri Dec 02 14:54:25 2011 +0100
    20.3 @@ -128,7 +128,7 @@
    20.4        (if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
    20.5  
    20.6  fun make_bool_args' xs =
    20.7 -  make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
    20.8 +  make_bool_args (K @{term False}) (K @{term True}) xs;
    20.9  
   20.10  fun arg_types_of k c = drop k (binder_types (fastype_of c));
   20.11  
   20.12 @@ -786,14 +786,14 @@
   20.13        in
   20.14          fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
   20.15            (Logic.strip_params r)
   20.16 -          (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
   20.17 +          (if null ps then @{term True} else foldr1 HOLogic.mk_conj ps)
   20.18        end;
   20.19  
   20.20      (* make a disjunction of all introduction rules *)
   20.21  
   20.22      val fp_fun =
   20.23        fold_rev lambda (p :: bs @ xs)
   20.24 -        (if null intr_ts then HOLogic.false_const
   20.25 +        (if null intr_ts then @{term False}
   20.26           else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
   20.27  
   20.28      (* add definiton of recursive predicates to theory *)
    21.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Dec 02 14:37:25 2011 +0100
    21.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Dec 02 14:54:25 2011 +0100
    21.3 @@ -56,7 +56,7 @@
    21.4  
    21.5  fun is_False thm =
    21.6    let val _ $ t = Thm.prop_of thm
    21.7 -  in t = HOLogic.false_const end;
    21.8 +  in t = @{term False} end;
    21.9  
   21.10  fun is_nat t = (fastype_of1 t = HOLogic.natT);
   21.11  
   21.12 @@ -349,7 +349,7 @@
   21.13    (* where ti' = HOLogic.dest_Trueprop ti                                    *)
   21.14    fun REPEAT_DETERM_etac_rev_mp tms =
   21.15      fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
   21.16 -      HOLogic.false_const
   21.17 +      @{term False}
   21.18    val split_thms  = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
   21.19    val cmap        = Splitter.cmap_of_split_thms split_thms
   21.20    val goal_tm     = REPEAT_DETERM_etac_rev_mp terms
   21.21 @@ -380,7 +380,7 @@
   21.22          val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   21.23                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   21.24          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   21.25 -        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.26 +        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.27          val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
   21.28          val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
   21.29        in
   21.30 @@ -395,7 +395,7 @@
   21.31          val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   21.32                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   21.33          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   21.34 -        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.35 +        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.36          val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
   21.37          val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
   21.38        in
   21.39 @@ -413,7 +413,7 @@
   21.40                              split_type --> split_type --> HOLogic.boolT) $ zero $ t1
   21.41          val t1_lt_zero  = Const (@{const_name Orderings.less},
   21.42                              split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
   21.43 -        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.44 +        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.45          val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
   21.46          val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
   21.47        in
   21.48 @@ -437,7 +437,7 @@
   21.49          val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   21.50                                  (Const (@{const_name Groups.plus},
   21.51                                    split_type --> split_type --> split_type) $ t2' $ d)
   21.52 -        val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.53 +        val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.54          val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
   21.55          val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
   21.56        in
   21.57 @@ -458,7 +458,7 @@
   21.58                              (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
   21.59          val t1_lt_zero  = Const (@{const_name Orderings.less},
   21.60                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   21.61 -        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.62 +        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.63          val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
   21.64          val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
   21.65        in
   21.66 @@ -488,7 +488,7 @@
   21.67                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   21.68                                           (Const (@{const_name Groups.times},
   21.69                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   21.70 -        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.71 +        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.72          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   21.73          val subgoal2                = (map HOLogic.mk_Trueprop
   21.74                                          [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
   21.75 @@ -520,7 +520,7 @@
   21.76                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   21.77                                           (Const (@{const_name Groups.times},
   21.78                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   21.79 -        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.80 +        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.81          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   21.82          val subgoal2                = (map HOLogic.mk_Trueprop
   21.83                                          [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
   21.84 @@ -566,7 +566,7 @@
   21.85                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   21.86                                           (Const (@{const_name Groups.times},
   21.87                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   21.88 -        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.89 +        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.90          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   21.91          val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
   21.92                                          @ hd terms2_3
   21.93 @@ -620,7 +620,7 @@
   21.94                                         (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   21.95                                           (Const (@{const_name Groups.times},
   21.96                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
   21.97 -        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   21.98 +        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   21.99          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  21.100          val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
  21.101                                          @ hd terms2_3
    22.1 --- a/src/HOL/Tools/prop_logic.ML	Fri Dec 02 14:37:25 2011 +0100
    22.2 +++ b/src/HOL/Tools/prop_logic.ML	Fri Dec 02 14:54:25 2011 +0100
    22.3 @@ -394,8 +394,8 @@
    22.4  (*       Boolean variables in the formula, similar to 'prop_formula_of_term' *)
    22.5  (*       (but the other way round).                                          *)
    22.6  
    22.7 -fun term_of_prop_formula True = HOLogic.true_const
    22.8 -  | term_of_prop_formula False = HOLogic.false_const
    22.9 +fun term_of_prop_formula True = @{term True}
   22.10 +  | term_of_prop_formula False = @{term False}
   22.11    | term_of_prop_formula (BoolVar i) = Free ("v" ^ string_of_int i, HOLogic.boolT)
   22.12    | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm)
   22.13    | term_of_prop_formula (Or (fm1, fm2)) =
    23.1 --- a/src/HOL/Tools/record.ML	Fri Dec 02 14:37:25 2011 +0100
    23.2 +++ b/src/HOL/Tools/record.ML	Fri Dec 02 14:54:25 2011 +0100
    23.3 @@ -1392,7 +1392,7 @@
    23.4               val prop =
    23.5                 list_all ([("r", T)],
    23.6                   Logic.mk_equals
    23.7 -                  (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
    23.8 +                  (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
    23.9              in SOME (prove prop) end
   23.10              handle TERM _ => NONE)
   23.11          | _ => NONE)
   23.12 @@ -1644,10 +1644,10 @@
   23.13      val inject_prop =  (* FIXME local x x' *)
   23.14        let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
   23.15          HOLogic.mk_conj (HOLogic.eq_const extT $
   23.16 -          mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
   23.17 +          mk_ext vars_more $ mk_ext vars_more', @{term True})
   23.18          ===
   23.19          foldr1 HOLogic.mk_conj
   23.20 -          (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
   23.21 +          (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
   23.22        end;
   23.23  
   23.24      val induct_prop =
    24.1 --- a/src/HOL/Tools/refute.ML	Fri Dec 02 14:37:25 2011 +0100
    24.2 +++ b/src/HOL/Tools/refute.ML	Fri Dec 02 14:54:25 2011 +0100
    24.3 @@ -2985,8 +2985,8 @@
    24.4      | Type ("prop", []) =>
    24.5          (case index_from_interpretation intr of
    24.6            ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
    24.7 -        | 0  => SOME (HOLogic.mk_Trueprop HOLogic.true_const)
    24.8 -        | 1  => SOME (HOLogic.mk_Trueprop HOLogic.false_const)
    24.9 +        | 0  => SOME (HOLogic.mk_Trueprop @{term True})
   24.10 +        | 1  => SOME (HOLogic.mk_Trueprop @{term False})
   24.11          | _  => raise REFUTE ("stlc_interpreter",
   24.12            "illegal interpretation for a propositional value"))
   24.13      | Type _  =>
    25.1 --- a/src/HOL/Tools/sat_funcs.ML	Fri Dec 02 14:37:25 2011 +0100
    25.2 +++ b/src/HOL/Tools/sat_funcs.ML	Fri Dec 02 14:54:25 2011 +0100
    25.3 @@ -288,7 +288,7 @@
    25.4    let
    25.5      (* remove premises that equal "True" *)
    25.6      val clauses' = filter (fn clause =>
    25.7 -      (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause
    25.8 +      (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
    25.9          handle TERM ("dest_Trueprop", _) => true) clauses
   25.10      (* remove non-clausal premises -- of course this shouldn't actually   *)
   25.11      (* remove anything as long as 'rawsat_tac' is only called after the   *)
   25.12 @@ -331,7 +331,7 @@
   25.13            if !trace_sat then
   25.14              tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
   25.15            else ()
   25.16 -        val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
   25.17 +        val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ @{term False})
   25.18        in
   25.19          (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
   25.20          (* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)