--- a/src/HOL/Decision_Procs/Cooper.thy Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Dec 02 14:54:25 2011 +0100
@@ -1943,8 +1943,8 @@
term_of_num vs (@{code C} i) $ term_of_num vs t2
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
-fun term_of_fm ps vs @{code T} = HOLogic.true_const
- | term_of_fm ps vs @{code F} = HOLogic.false_const
+fun term_of_fm ps vs @{code T} = @{term True}
+ | term_of_fm ps vs @{code F} = @{term False}
| term_of_fm ps vs (@{code Lt} t) =
@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::int"}
| term_of_fm ps vs (@{code Le} t) =
--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Dec 02 14:54:25 2011 +0100
@@ -1976,8 +1976,8 @@
term_of_num vs (@{code C} i) $ term_of_num vs t2
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
-fun term_of_fm vs @{code T} = HOLogic.true_const
- | term_of_fm vs @{code F} = HOLogic.false_const
+fun term_of_fm vs @{code T} = @{term True}
+ | term_of_fm vs @{code F} = @{term False}
| term_of_fm vs (@{code Lt} t) = @{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $
term_of_num vs t $ @{term "0::real"}
| term_of_fm vs (@{code Le} t) = @{term "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool"} $
--- a/src/HOL/Decision_Procs/MIR.thy Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Dec 02 14:54:25 2011 +0100
@@ -5602,8 +5602,8 @@
| term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t))
| term_of_num vs (@{code CF} (c, t, s)) = term_of_num vs (@{code Add} (@{code Mul} (c, @{code Floor} t), s));
-fun term_of_fm vs @{code T} = HOLogic.true_const
- | term_of_fm vs @{code F} = HOLogic.false_const
+fun term_of_fm vs @{code T} = @{term True}
+ | term_of_fm vs @{code F} = @{term False}
| term_of_fm vs (@{code Lt} t) =
@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ term_of_num vs t $ @{term "0::real"}
| term_of_fm vs (@{code Le} t) =
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Dec 02 14:54:25 2011 +0100
@@ -1025,7 +1025,7 @@
Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(fresh c,
- if null dts then HOLogic.true_const
+ if null dts then @{term True}
else foldr1 HOLogic.mk_conj (map fresh args2)))))
(fn _ =>
simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
--- a/src/HOL/Nominal/nominal_primrec.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Dec 02 14:54:25 2011 +0100
@@ -308,7 +308,7 @@
curry (List.take o swap) (length fvars) |> map cert;
val invs' = (case invs of
NONE => map (fn (i, _) =>
- Abs ("x", fastype_of (snd (nth defs' i)), HOLogic.true_const)) descr
+ Abs ("x", fastype_of (snd (nth defs' i)), @{term True})) descr
| SOME invs' => map (prep_term lthy') invs');
val inst = (map cert fvars ~~ cfs) @
(map (cert o Var) pvars ~~ map cert invs') @
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Dec 02 14:54:25 2011 +0100
@@ -1003,8 +1003,8 @@
val (((defs', vars''), ivars), (ids, thy')) =
((Symtab.empty |>
- Symtab.update ("false", (HOLogic.false_const, booleanN)) |>
- Symtab.update ("true", (HOLogic.true_const, booleanN)),
+ Symtab.update ("false", (@{term False}, booleanN)) |>
+ Symtab.update ("true", (@{term True}, booleanN)),
Name.context),
thy |> Sign.add_path (Long_Name.base_name ident)) |>
fold (add_type_def prfx) (items types) |>
--- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Fri Dec 02 14:54:25 2011 +0100
@@ -29,6 +29,7 @@
datatype direction = Left | Right;
fun treeT T = Type (@{type_name tree}, [T]);
+
fun mk_tree' e T n [] = Const (@{const_name Tip}, treeT T)
| mk_tree' e T n xs =
let
@@ -38,7 +39,7 @@
val r = mk_tree' e T (n-(m+1)) xsr;
in
Const (@{const_name Node}, treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $
- l $ e x $ HOLogic.false_const $ r
+ l $ e x $ @{term False} $ r
end
fun mk_tree e T xs = mk_tree' e T (length xs) xs;
--- a/src/HOL/Statespace/state_fun.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML Fri Dec 02 14:54:25 2011 +0100
@@ -309,7 +309,7 @@
val (eq, eT, nT, swap) = mkeq (dest_sel_eq t) 0;
val prop =
list_all ([("n", nT), ("x", eT)],
- Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
+ Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
val thm = Drule.export_without_context (prove prop);
val thm' = if swap then swap_ex_eq OF [thm] else thm
in SOME thm' end handle TERM _ => NONE)
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Dec 02 14:54:25 2011 +0100
@@ -586,7 +586,7 @@
(* No "real" literals means only type information (tfree_tcs, clsrel, or
clsarity). *)
-val is_only_type_information = curry (op aconv) HOLogic.true_const
+val is_only_type_information = curry (op aconv) @{term True}
fun replace_one_dependency (old, new) dep =
if is_same_atp_step dep old then new else [dep]
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Dec 02 14:54:25 2011 +0100
@@ -478,7 +478,7 @@
let val isoT = T --> Univ_elT in
HOLogic.imp $
(Const (set_name, UnivT') $ Datatype_Aux.mk_Free "x" Univ_elT i) $
- (if i < length newTs then HOLogic.true_const
+ (if i < length newTs then @{term True}
else HOLogic.mk_mem (Datatype_Aux.mk_Free "x" Univ_elT i,
Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $
Const (iso_name, isoT) $ Const (@{const_abbrev UNIV}, HOLogic.mk_setT T)))
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Dec 02 14:54:25 2011 +0100
@@ -68,8 +68,8 @@
Datatype_Data.the_info thy tyco;
val ty = Type (tyco, map TFree vs);
fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT) $ t1 $ t2;
- fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
- fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
+ fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term True});
+ fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term False});
val triv_injects =
map_filter
(fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
--- a/src/HOL/Tools/Function/lexicographic_order.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri Dec 02 14:54:25 2011 +0100
@@ -79,7 +79,7 @@
(case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
- if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
+ if prems_of thm2 = [HOLogic.Trueprop $ @{term False}] then False thm2
else None (thm2, thm)
| _ => raise Match) (* FIXME *)
| _ => raise Match
--- a/src/HOL/Tools/Function/size.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML Fri Dec 02 14:54:25 2011 +0100
@@ -160,7 +160,7 @@
fun prove_unfolded_size_eqs size_ofp fs =
if null recTs2 then []
else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs []
- (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l HOLogic.true_const @
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @
map (mk_unfolded_size_eq (AList.lookup op =
(new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
(xs ~~ recTs2 ~~ rec_combs2))))
--- a/src/HOL/Tools/Function/termination.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Function/termination.ML Fri Dec 02 14:54:25 2011 +0100
@@ -182,7 +182,7 @@
(case try @{const_name Orderings.less_eq} of
Solved thm2 => LessEq (thm2, thm)
| Stuck thm2 =>
- if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
+ if prems_of thm2 = [HOLogic.Trueprop $ @{term False}]
then False thm2 else None (thm2, thm)
| _ => raise Match) (* FIXME *)
| _ => raise Match
@@ -260,7 +260,7 @@
val pT = HOLogic.mk_prodT (T, T)
val n = length qs
val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
- val conds' = if null conds then [HOLogic.true_const] else conds
+ val conds' = if null conds then [@{term True}] else conds
in
HOLogic.Collect_const pT $
Abs ("uu_", pT,
--- a/src/HOL/Tools/Meson/meson.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Fri Dec 02 14:54:25 2011 +0100
@@ -231,7 +231,7 @@
let val (poslits,neglits) = signed_lits th
in exists taut_poslit poslits
orelse
- exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
+ exists (member (op aconv) neglits) (@{term False} :: poslits)
end
handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Dec 02 14:54:25 2011 +0100
@@ -35,8 +35,8 @@
(**** Transformation of Elimination Rules into First-Order Formulas****)
-val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
-val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
+val cfalse = cterm_of @{theory HOL} @{term False};
+val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop @{term False});
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Dec 02 14:54:25 2011 +0100
@@ -653,8 +653,8 @@
| term_of_num vs (Proc.Cn (n, i, t')) =
term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
-fun term_of_fm ps vs Proc.T = HOLogic.true_const
- | term_of_fm ps vs Proc.F = HOLogic.false_const
+fun term_of_fm ps vs Proc.T = @{term True}
+ | term_of_fm ps vs Proc.F = @{term False}
| term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
| term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
| term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
--- a/src/HOL/Tools/cnf_funcs.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Dec 02 14:54:25 2011 +0100
@@ -294,18 +294,18 @@
val thm1 = simp_True_False_thm thy x
val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
in
- if x' = HOLogic.false_const then
+ if x' = @{term False} then
simp_TF_conj_False_l OF [thm1] (* (x & y) = False *)
else
let
val thm2 = simp_True_False_thm thy y
val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
in
- if x' = HOLogic.true_const then
+ if x' = @{term True} then
simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *)
- else if y' = HOLogic.false_const then
+ else if y' = @{term False} then
simp_TF_conj_False_r OF [thm2] (* (x & y) = False *)
- else if y' = HOLogic.true_const then
+ else if y' = @{term True} then
simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *)
else
conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *)
@@ -316,18 +316,18 @@
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
in
- if x' = HOLogic.true_const then
+ if x' = @{term True} then
simp_TF_disj_True_l OF [thm1] (* (x | y) = True *)
else
let
val thm2 = simp_True_False_thm thy y
val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
in
- if x' = HOLogic.false_const then
+ if x' = @{term False} then
simp_TF_disj_False_l OF [thm1, thm2] (* (x | y) = y' *)
- else if y' = HOLogic.true_const then
+ else if y' = @{term True} then
simp_TF_disj_True_r OF [thm2] (* (x | y) = True *)
- else if y' = HOLogic.false_const then
+ else if y' = @{term False} then
simp_TF_disj_False_r OF [thm1, thm2] (* (x | y) = x' *)
else
disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *)
--- a/src/HOL/Tools/hologic.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/hologic.ML Fri Dec 02 14:54:25 2011 +0100
@@ -15,8 +15,6 @@
val Trueprop: term
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
- val true_const: term
- val false_const: term
val mk_induct_forall: typ -> term
val mk_setT: typ -> typ
val dest_setT: typ -> typ
@@ -162,9 +160,6 @@
val boolN = "HOL.bool";
val boolT = Type (boolN, []);
-val true_const = Const ("HOL.True", boolT);
-val false_const = Const ("HOL.False", boolT);
-
fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
fun mk_setT T = T --> boolT;
--- a/src/HOL/Tools/inductive.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Dec 02 14:54:25 2011 +0100
@@ -128,7 +128,7 @@
(if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
fun make_bool_args' xs =
- make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
+ make_bool_args (K @{term False}) (K @{term True}) xs;
fun arg_types_of k c = drop k (binder_types (fastype_of c));
@@ -786,14 +786,14 @@
in
fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
(Logic.strip_params r)
- (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
+ (if null ps then @{term True} else foldr1 HOLogic.mk_conj ps)
end;
(* make a disjunction of all introduction rules *)
val fp_fun =
fold_rev lambda (p :: bs @ xs)
- (if null intr_ts then HOLogic.false_const
+ (if null intr_ts then @{term False}
else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
(* add definiton of recursive predicates to theory *)
--- a/src/HOL/Tools/lin_arith.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/lin_arith.ML Fri Dec 02 14:54:25 2011 +0100
@@ -56,7 +56,7 @@
fun is_False thm =
let val _ $ t = Thm.prop_of thm
- in t = HOLogic.false_const end;
+ in t = @{term False} end;
fun is_nat t = (fastype_of1 t = HOLogic.natT);
@@ -349,7 +349,7 @@
(* where ti' = HOLogic.dest_Trueprop ti *)
fun REPEAT_DETERM_etac_rev_mp tms =
fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
- HOLogic.false_const
+ @{term False}
val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
val cmap = Splitter.cmap_of_split_thms split_thms
val goal_tm = REPEAT_DETERM_etac_rev_mp terms
@@ -380,7 +380,7 @@
val t1_leq_t2 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
in
@@ -395,7 +395,7 @@
val t1_leq_t2 = Const (@{const_name Orderings.less_eq},
split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
in
@@ -413,7 +413,7 @@
split_type --> split_type --> HOLogic.boolT) $ zero $ t1
val t1_lt_zero = Const (@{const_name Orderings.less},
split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
in
@@ -437,7 +437,7 @@
val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const (@{const_name Groups.plus},
split_type --> split_type --> split_type) $ t2' $ d)
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
in
@@ -458,7 +458,7 @@
(Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
val t1_lt_zero = Const (@{const_name Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
in
@@ -488,7 +488,7 @@
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
val subgoal2 = (map HOLogic.mk_Trueprop
[t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
@@ -520,7 +520,7 @@
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
val subgoal2 = (map HOLogic.mk_Trueprop
[t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
@@ -566,7 +566,7 @@
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
val subgoal2 = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
@ hd terms2_3
@@ -620,7 +620,7 @@
(Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
(Const (@{const_name Groups.times},
split_type --> split_type --> split_type) $ t2' $ i) $ j)
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
val subgoal2 = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
@ hd terms2_3
--- a/src/HOL/Tools/prop_logic.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/prop_logic.ML Fri Dec 02 14:54:25 2011 +0100
@@ -394,8 +394,8 @@
(* Boolean variables in the formula, similar to 'prop_formula_of_term' *)
(* (but the other way round). *)
-fun term_of_prop_formula True = HOLogic.true_const
- | term_of_prop_formula False = HOLogic.false_const
+fun term_of_prop_formula True = @{term True}
+ | term_of_prop_formula False = @{term False}
| term_of_prop_formula (BoolVar i) = Free ("v" ^ string_of_int i, HOLogic.boolT)
| term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm)
| term_of_prop_formula (Or (fm1, fm2)) =
--- a/src/HOL/Tools/record.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/record.ML Fri Dec 02 14:54:25 2011 +0100
@@ -1392,7 +1392,7 @@
val prop =
list_all ([("r", T)],
Logic.mk_equals
- (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
+ (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
in SOME (prove prop) end
handle TERM _ => NONE)
| _ => NONE)
@@ -1644,10 +1644,10 @@
val inject_prop = (* FIXME local x x' *)
let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
HOLogic.mk_conj (HOLogic.eq_const extT $
- mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
+ mk_ext vars_more $ mk_ext vars_more', @{term True})
===
foldr1 HOLogic.mk_conj
- (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
+ (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
end;
val induct_prop =
--- a/src/HOL/Tools/refute.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/refute.ML Fri Dec 02 14:54:25 2011 +0100
@@ -2985,8 +2985,8 @@
| Type ("prop", []) =>
(case index_from_interpretation intr of
~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
- | 0 => SOME (HOLogic.mk_Trueprop HOLogic.true_const)
- | 1 => SOME (HOLogic.mk_Trueprop HOLogic.false_const)
+ | 0 => SOME (HOLogic.mk_Trueprop @{term True})
+ | 1 => SOME (HOLogic.mk_Trueprop @{term False})
| _ => raise REFUTE ("stlc_interpreter",
"illegal interpretation for a propositional value"))
| Type _ =>
--- a/src/HOL/Tools/sat_funcs.ML Fri Dec 02 14:37:25 2011 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Fri Dec 02 14:54:25 2011 +0100
@@ -288,7 +288,7 @@
let
(* remove premises that equal "True" *)
val clauses' = filter (fn clause =>
- (not_equal HOLogic.true_const o HOLogic.dest_Trueprop o Thm.term_of) clause
+ (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
handle TERM ("dest_Trueprop", _) => true) clauses
(* remove non-clausal premises -- of course this shouldn't actually *)
(* remove anything as long as 'rawsat_tac' is only called after the *)
@@ -331,7 +331,7 @@
if !trace_sat then
tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
else ()
- val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
+ val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ @{term False})
in
(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *)
(* Thm.weaken sorted_clauses' would be quadratic, since we sorted *)