# HG changeset patch # User wenzelm # Date 1322834065 -3600 # Node ID 132a3e1c0fe50ef3bc991c5919e5142dfd980309 # Parent b545ea8bc731843bd470e430ad3c79858feadfd1 more antiquotations; diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Decision_Procs/Cooper.thy --- 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 \ int \ bool"} $ term_of_num vs t $ @{term "0::int"} | term_of_fm ps vs (@{code Le} t) = diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Decision_Procs/Ferrack.thy --- 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 \ real \ bool"} $ term_of_num vs t $ @{term "0::real"} | term_of_fm vs (@{code Le} t) = @{term "op \ :: real \ real \ bool"} $ diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Decision_Procs/MIR.thy --- 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 \ real \ bool"} $ term_of_num vs t $ @{term "0::real"} | term_of_fm vs (@{code Le} t) = diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Nominal/nominal_datatype.ML --- 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)) diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Nominal/nominal_primrec.ML --- 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') @ diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/SPARK/Tools/spark_vcs.ML --- 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) |> diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Statespace/distinct_tree_prover.ML --- 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; diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Statespace/state_fun.ML --- 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) diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/ATP/atp_reconstruct.ML --- 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] diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Datatype/datatype.ML --- 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))) diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Datatype/datatype_codegen.ML --- 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)))) diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Function/lexicographic_order.ML --- 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 diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Function/size.ML --- 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)))) diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Function/termination.ML --- 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, diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Meson/meson.ML --- 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*) diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Meson/meson_clausify.ML --- 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 diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/cnf_funcs.ML --- 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') *) diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/hologic.ML --- 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; diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/inductive.ML --- 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 *) diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/lin_arith.ML --- 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 diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/prop_logic.ML --- 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)) = diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/record.ML --- 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 = diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/refute.ML --- 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 _ => diff -r b545ea8bc731 -r 132a3e1c0fe5 src/HOL/Tools/sat_funcs.ML --- 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 *)