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 *)