--- a/src/HOL/Decision_Procs/Approximation.thy Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Aug 19 16:08:59 2010 +0200
@@ -3301,10 +3301,10 @@
ML {*
fun reorder_bounds_tac prems i =
let
- fun variable_of_bound (Const (@{const_name "Trueprop"}, _) $
+ fun variable_of_bound (Const (@{const_name Trueprop}, _) $
(Const (@{const_name Set.member}, _) $
Free (name, _) $ _)) = name
- | variable_of_bound (Const (@{const_name "Trueprop"}, _) $
+ | variable_of_bound (Const (@{const_name Trueprop}, _) $
(Const (@{const_name "op ="}, _) $
Free (name, _) $ _)) = name
| variable_of_bound t = raise TERM ("variable_of_bound", [t])
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Thu Aug 19 16:08:59 2010 +0200
@@ -1960,12 +1960,12 @@
@{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term ps vs t')
- | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
+ | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
let
val (xn', p') = variant_abs (xn, xT, p);
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code E} (fm_of_term ps vs' p) end
- | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
+ | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
let
val (xn', p') = variant_abs (xn, xT, p);
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Aug 19 16:08:59 2010 +0200
@@ -2000,9 +2000,9 @@
| fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (("", dummyT) :: vs) p)
- | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (("", dummyT) :: vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
--- a/src/HOL/Decision_Procs/MIR.thy Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Aug 19 16:08:59 2010 +0200
@@ -5845,9 +5845,9 @@
@{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
| fm_of_term vs (@{term "Not"} $ t') =
@{code NOT} (fm_of_term vs t')
- | fm_of_term vs (Const (@{const_name "Ex"}, _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
@{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
- | fm_of_term vs (Const (@{const_name "All"}, _) $ Abs (xn, xT, p)) =
+ | fm_of_term vs (Const (@{const_name All}, _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
| fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Aug 19 16:08:59 2010 +0200
@@ -3015,9 +3015,9 @@
fun fm_of_term m m' fm =
case fm of
- Const(@{const_name "True"},_) => @{code T}
- | Const(@{const_name "False"},_) => @{code F}
- | Const(@{const_name "Not"},_)$p => @{code NOT} (fm_of_term m m' p)
+ Const(@{const_name True},_) => @{code T}
+ | Const(@{const_name False},_) => @{code F}
+ | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
| Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
| Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
@@ -3028,13 +3028,13 @@
@{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
| Const(@{const_name Orderings.less_eq},_)$p$q =>
@{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
- | Const(@{const_name "Ex"},_)$Abs(xn,xT,p) =>
+ | Const(@{const_name Ex},_)$Abs(xn,xT,p) =>
let val (xn', p') = variant_abs (xn,xT,p)
val x = Free(xn',xT)
fun incr i = i + 1
val m0 = (x,0):: (map (apsnd incr) m)
in @{code E} (fm_of_term m0 m' p') end
- | Const(@{const_name "All"},_)$Abs(xn,xT,p) =>
+ | Const(@{const_name All},_)$Abs(xn,xT,p) =>
let val (xn', p') = variant_abs (xn,xT,p)
val x = Free(xn',xT)
fun incr i = i + 1
@@ -3045,8 +3045,8 @@
fun term_of_fm T m m' t =
case t of
- @{code T} => Const(@{const_name "True"},bT)
- | @{code F} => Const(@{const_name "False"},bT)
+ @{code T} => Const(@{const_name True},bT)
+ | @{code F} => Const(@{const_name False},bT)
| @{code NOT} p => nott $ (term_of_fm T m m' p)
| @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
| @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
--- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Thu Aug 19 16:08:59 2010 +0200
@@ -110,7 +110,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
- Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
in
((pth RS iffD2) RS pre_thm,
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Thu Aug 19 16:08:59 2010 +0200
@@ -91,7 +91,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case prop_of pre_thm of
- Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Aug 19 16:08:59 2010 +0200
@@ -77,7 +77,7 @@
fun main vs p =
let
val ((xn,ce),(x,fm)) = (case term_of p of
- Const(@{const_name "Ex"},_)$Abs(xn,xT,_) =>
+ Const(@{const_name Ex},_)$Abs(xn,xT,_) =>
Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn
| _ => raise CTERM ("main QE only treats existential quantifiers!", [p]))
val cT = ctyp_of_term x
@@ -178,16 +178,16 @@
Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
- | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
- | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm)
--- a/src/HOL/Decision_Procs/langford.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Thu Aug 19 16:08:59 2010 +0200
@@ -30,7 +30,7 @@
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
case term_of ep of
- Const(@{const_name "Ex"},_)$_ =>
+ Const(@{const_name Ex},_)$_ =>
let
val p = Thm.dest_arg ep
val ths = simplify (HOL_basic_ss addsimps gather) (instantiate' [] [SOME p] stupid)
@@ -122,7 +122,7 @@
local
fun proc ct =
case term_of ct of
- Const(@{const_name "Ex"},_)$Abs (xn,_,_) =>
+ Const(@{const_name Ex},_)$Abs (xn,_,_) =>
let
val e = Thm.dest_fun ct
val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
@@ -179,16 +179,16 @@
Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else Thm.dest_fun2 tm
- | Const (@{const_name "Not"}, _) $ _ => h bounds (Thm.dest_arg tm)
- | Const (@{const_name "All"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
| Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
| Const ("==>", _) $ _ $ _ => find_args bounds tm
| Const ("==", _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name "Trueprop"}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
| _ => Thm.dest_fun2 tm)
and find_args bounds tm =
(h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
--- a/src/HOL/Decision_Procs/mir_tac.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Thu Aug 19 16:08:59 2010 +0200
@@ -132,7 +132,7 @@
fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
- Const ("==>", _) $ (Const (@{const_name "Trueprop"}, _) $ t1) $ _ =>
+ Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
if !quick_and_dirty
--- a/src/HOL/Import/shuffler.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Thu Aug 19 16:08:59 2010 +0200
@@ -60,14 +60,14 @@
fun mk_meta_eq th =
(case concl_of th of
- Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
+ Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th RS eq_reflection
| Const("==",_) $ _ $ _ => th
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make meta equality",0,[th]) (* FIXME avoid handle _ *)
fun mk_obj_eq th =
(case concl_of th of
- Const(@{const_name "Trueprop"},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
+ Const(@{const_name Trueprop},_) $ (Const(@{const_name "op ="},_) $ _ $ _) => th
| Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
--- a/src/HOL/Library/Eval_Witness.thy Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Thu Aug 19 16:08:59 2010 +0200
@@ -63,7 +63,7 @@
else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
fun dest_exs 0 t = t
- | dest_exs n (Const (@{const_name "Ex"}, _) $ Abs (v,T,b)) =
+ | dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) =
Abs (v, check_type T, dest_exs (n - 1) b)
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
--- a/src/HOL/Library/positivstellensatz.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Thu Aug 19 16:08:59 2010 +0200
@@ -498,7 +498,7 @@
val strip_exists =
let fun h (acc, t) =
case (term_of t) of
- Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name Ex},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
@@ -515,7 +515,7 @@
fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
fun choose v th th' = case concl_of th of
- @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) =>
+ @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o cprop_of) th
val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -533,7 +533,7 @@
val strip_forall =
let fun h (acc, t) =
case (term_of t) of
- Const(@{const_name "All"},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name All},_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Aug 19 16:08:59 2010 +0200
@@ -183,7 +183,7 @@
end;
fun mk_not_sym ths = maps (fn th => case prop_of th of
- _ $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
+ _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) => [th, th RS not_sym]
| _ => [th]) ths;
fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
@@ -1372,7 +1372,7 @@
SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
_ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
simp_tac ind_ss1' i
- | _ $ (Const (@{const_name "Not"}, _) $ _) =>
+ | _ $ (Const (@{const_name Not}, _) $ _) =>
resolve_tac freshs2' i
| _ => asm_simp_tac (HOL_basic_ss addsimps
pt2_atoms addsimprocs [perm_simproc]) i)) 1])
@@ -1671,7 +1671,7 @@
val rec_unique_frees' =
Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
val rec_unique_concls = map (fn ((x, U), R) =>
- Const (@{const_name "Ex1"}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
+ Const (@{const_name Ex1}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
Abs ("y", U, R $ Free x $ Bound 0))
(rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
@@ -1777,7 +1777,7 @@
| _ => false) prems';
val fresh_prems = filter (fn th => case prop_of th of
_ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
- | _ $ (Const (@{const_name "Not"}, _) $ _) => true
+ | _ $ (Const (@{const_name Not}, _) $ _) => true
| _ => false) prems';
val Ts = map fastype_of boundsl;
@@ -1879,7 +1879,7 @@
end) rec_prems2;
val ihs = filter (fn th => case prop_of th of
- _ $ (Const (@{const_name "All"}, _) $ _) => true | _ => false) prems';
+ _ $ (Const (@{const_name All}, _) $ _) => true | _ => false) prems';
(** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
@@ -2022,7 +2022,7 @@
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
(Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
- Const (@{const_name "The"}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
+ Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Aug 19 16:08:59 2010 +0200
@@ -78,7 +78,7 @@
| split_conj _ _ _ _ = NONE;
fun strip_all [] t = t
- | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
+ | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
(*********************************************************************)
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *)
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Aug 19 16:08:59 2010 +0200
@@ -82,7 +82,7 @@
| split_conj _ _ _ _ = NONE;
fun strip_all [] t = t
- | strip_all (_ :: xs) (Const (@{const_name "All"}, _) $ Abs (s, T, t)) = strip_all xs t;
+ | strip_all (_ :: xs) (Const (@{const_name All}, _) $ Abs (s, T, t)) = strip_all xs t;
(*********************************************************************)
(* maps R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)) *)
--- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Aug 19 16:08:59 2010 +0200
@@ -135,7 +135,7 @@
val thy = Context.theory_of context
val thms_to_be_added = (case (prop_of orig_thm) of
(* case: eqvt-lemma is of the implicational form *)
- (Const("==>", _) $ (Const (@{const_name "Trueprop"},_) $ hyp) $ (Const (@{const_name "Trueprop"},_) $ concl)) =>
+ (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
let
val (pi,typi) = get_pi concl thy
in
@@ -147,7 +147,7 @@
else raise EQVT_FORM "Type Implication"
end
(* case: eqvt-lemma is of the equational form *)
- | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
+ | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
(Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]
--- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Thu Aug 19 16:08:59 2010 +0200
@@ -343,7 +343,7 @@
end handle Option => NONE)
fun distinctTree_tac names ctxt
- (Const (@{const_name "Trueprop"},_) $ (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
+ (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ x $ y)), i) =
(case get_fst_success (neq_x_y ctxt x y) names of
SOME neq => rtac neq i
| NONE => no_tac)
--- a/src/HOL/Statespace/state_fun.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML Thu Aug 19 16:08:59 2010 +0200
@@ -43,9 +43,9 @@
val conj_True = thm "conj_True";
val conj_cong = thm "conj_cong";
-fun isFalse (Const (@{const_name "False"},_)) = true
+fun isFalse (Const (@{const_name False},_)) = true
| isFalse _ = false;
-fun isTrue (Const (@{const_name "True"},_)) = true
+fun isTrue (Const (@{const_name True},_)) = true
| isTrue _ = false;
in
@@ -305,10 +305,10 @@
in
(case t of
- (Const (@{const_name "Ex"},Tex)$Abs(s,T,t)) =>
+ (Const (@{const_name Ex},Tex)$Abs(s,T,t)) =>
(let 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),
+ Logic.mk_equals (Const (@{const_name Ex},Tex)$Abs(s,T,eq),
HOLogic.true_const));
val thm = Drule.export_without_context (prove prop);
val thm' = if swap then swap_ex_eq OF [thm] else thm
@@ -367,7 +367,7 @@
val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
val (lookup_ss', ex_lookup_ss') =
(case (concl_of thm) of
- (_$((Const (@{const_name "Ex"},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
+ (_$((Const (@{const_name Ex},_)$_))) => (lookup_ss, ex_lookup_ss addsimps [thm])
| _ => (lookup_ss addsimps [thm], ex_lookup_ss))
fun activate_simprocs ctxt =
if simprocs_active then ctxt
--- a/src/HOL/Statespace/state_space.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Aug 19 16:08:59 2010 +0200
@@ -222,8 +222,8 @@
end handle Option => NONE)
fun distinctTree_tac ctxt
- (Const (@{const_name "Trueprop"},_) $
- (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
+ (Const (@{const_name Trueprop},_) $
+ (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, _) $ (x as Free _)$ (y as Free _))), i) =
(case (neq_x_y ctxt x y) of
SOME neq => rtac neq i
| NONE => no_tac)
--- a/src/HOL/Tools/Function/function_core.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Thu Aug 19 16:08:59 2010 +0200
@@ -392,7 +392,7 @@
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
val ihyp = Term.all domT $ Abs ("z", domT,
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
- HOLogic.mk_Trueprop (Const (@{const_name "Ex1"}, (ranT --> boolT) --> boolT) $
+ HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $
Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
|> cterm_of thy
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 19 16:08:59 2010 +0200
@@ -147,7 +147,7 @@
fun Trueprop_conv cv ct =
case Thm.term_of ct of
- Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
| _ => raise Fail "Trueprop_conv"
fun preprocess_intro thy rule =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Aug 19 16:08:59 2010 +0200
@@ -411,7 +411,7 @@
fun conjuncts t = conjuncts_aux t [];
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
- | is_equationlike_term (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
+ | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _)) = true
| is_equationlike_term _ = false
val is_equationlike = is_equationlike_term o prop_of
@@ -479,7 +479,7 @@
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
-fun strip_ex (Const (@{const_name "Ex"}, _) $ Abs (x, T, t)) =
+fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
let
val (xTs, t') = strip_ex t
in
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 19 16:08:59 2010 +0200
@@ -576,7 +576,7 @@
fun Trueprop_conv cv ct =
case Thm.term_of ct of
- Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
| _ => raise Fail "Trueprop_conv"
fun preprocess_intro thy rule =
@@ -587,7 +587,7 @@
fun preprocess_elim ctxt elimrule =
let
- fun replace_eqs (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
+ fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =
HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
| replace_eqs t = t
val thy = ProofContext.theory_of ctxt
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 19 16:08:59 2010 +0200
@@ -111,7 +111,7 @@
fun mk_meta_equation th =
case prop_of th of
- Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ _) => th RS @{thm eq_reflection}
| _ => th
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -215,12 +215,12 @@
val logic_operator_names =
[@{const_name "=="},
@{const_name "==>"},
- @{const_name "Trueprop"},
- @{const_name "Not"},
+ @{const_name Trueprop},
+ @{const_name Not},
@{const_name "op ="},
@{const_name "op -->"},
- @{const_name "All"},
- @{const_name "Ex"},
+ @{const_name All},
+ @{const_name Ex},
@{const_name "op &"},
@{const_name "op |"}]
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Aug 19 16:08:59 2010 +0200
@@ -86,9 +86,9 @@
map instantiate rew_ths
end
-fun is_compound ((Const (@{const_name "Not"}, _)) $ t) =
+fun is_compound ((Const (@{const_name Not}, _)) $ t) =
error "is_compound: Negation should not occur; preprocessing is defect"
- | is_compound ((Const (@{const_name "Ex"}, _)) $ _) = true
+ | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
| is_compound ((Const (@{const_name "op |"}, _)) $ _ $ _) = true
| is_compound ((Const (@{const_name "op &"}, _)) $ _ $ _) =
error "is_compound: Conjunction should not occur; preprocessing is defect"
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Aug 19 16:08:59 2010 +0200
@@ -622,9 +622,9 @@
Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
| fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
Proc.Not (fm_of_term ps vs t')
- | fm_of_term ps vs (Const (@{const_name "Ex"}, _) $ Abs abs) =
+ | fm_of_term ps vs (Const (@{const_name Ex}, _) $ Abs abs) =
Proc.E (uncurry (fm_of_term ps) (descend vs abs))
- | fm_of_term ps vs (Const (@{const_name "All"}, _) $ Abs abs) =
+ | fm_of_term ps vs (Const (@{const_name All}, _) $ Abs abs) =
Proc.A (uncurry (fm_of_term ps) (descend vs abs))
| fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
@@ -694,7 +694,7 @@
fun strip_objall ct =
case term_of ct of
- Const (@{const_name "All"}, _) $ Abs (xn,xT,p) =>
+ Const (@{const_name All}, _) $ Abs (xn,xT,p) =>
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
in apfst (cons (a,v)) (strip_objall t')
end
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 19 16:08:59 2010 +0200
@@ -490,16 +490,16 @@
else mk_bex1_rel $ resrel $ subtrm
end
- | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+ | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
in
- if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
+ if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
| (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
- Const (@{const_name "All"}, ty') $ t') =>
+ Const (@{const_name All}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -510,7 +510,7 @@
end
| (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
- Const (@{const_name "Ex"}, ty') $ t') =>
+ Const (@{const_name Ex}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -520,7 +520,7 @@
else mk_bex $ (mk_resp $ resrel) $ subtrm
end
- | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+ | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -638,10 +638,10 @@
as the type of subterms needs to be calculated *)
fun inj_repabs_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
- (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+ (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
- | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+ | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
| (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
--- a/src/HOL/Tools/choice_specification.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Thu Aug 19 16:08:59 2010 +0200
@@ -24,7 +24,7 @@
fun mk_definitional [] arg = arg
| mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
case HOLogic.dest_Trueprop (concl_of thm) of
- Const(@{const_name "Ex"},_) $ P =>
+ Const(@{const_name Ex},_) $ P =>
let
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
@@ -51,7 +51,7 @@
end
| process ((thname,cname,covld)::cos) (thy,tm) =
case tm of
- Const(@{const_name "Ex"},_) $ P =>
+ Const(@{const_name Ex},_) $ P =>
let
val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
--- a/src/HOL/Tools/cnf_funcs.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Aug 19 16:08:59 2010 +0200
@@ -93,16 +93,16 @@
val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto};
-fun is_atom (Const (@{const_name "False"}, _)) = false
- | is_atom (Const (@{const_name "True"}, _)) = false
+fun is_atom (Const (@{const_name False}, _)) = false
+ | is_atom (Const (@{const_name True}, _)) = false
| is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false
| is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
- | is_atom (Const (@{const_name "Not"}, _) $ _) = false
+ | is_atom (Const (@{const_name Not}, _) $ _) = false
| is_atom _ = true;
-fun is_literal (Const (@{const_name "Not"}, _) $ x) = is_atom x
+fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
| is_literal x = is_atom x;
fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
@@ -118,7 +118,7 @@
fun clause_is_trivial c =
let
(* Term.term -> Term.term *)
- fun dual (Const (@{const_name "Not"}, _) $ x) = x
+ fun dual (Const (@{const_name Not}, _) $ x) = x
| dual x = HOLogic.Not $ x
(* Term.term list -> bool *)
fun has_duals [] = false
@@ -214,32 +214,32 @@
in
make_nnf_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "False"}, _)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
make_nnf_not_false
- | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "True"}, _)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
make_nnf_not_true
- | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_conj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_disj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -248,7 +248,7 @@
in
make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "Not"}, _) $ x)) =
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
let
val thm1 = make_nnf_thm thy x
in
@@ -430,7 +430,7 @@
in
make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
end
- | make_cnfx_disj_thm (Const (@{const_name "Ex"}, _) $ x') y' =
+ | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
val var = new_free ()
@@ -441,7 +441,7 @@
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
- | make_cnfx_disj_thm x' (Const (@{const_name "Ex"}, _) $ y') =
+ | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
val var = new_free ()
--- a/src/HOL/Tools/groebner.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/groebner.ML Thu Aug 19 16:08:59 2010 +0200
@@ -405,7 +405,7 @@
val mk_comb = capply;
fun is_neg t =
case term_of t of
- (Const(@{const_name "Not"},_)$p) => true
+ (Const(@{const_name Not},_)$p) => true
| _ => false;
fun is_eq t =
case term_of t of
@@ -430,14 +430,14 @@
val strip_exists =
let fun h (acc, t) =
case (term_of t) of
- Const(@{const_name "Ex"},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
+ Const(@{const_name Ex},_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
end;
fun is_forall t =
case term_of t of
- (Const(@{const_name "All"},_)$Abs(_,_,_)) => true
+ (Const(@{const_name All},_)$Abs(_,_,_)) => true
| _ => false;
val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
@@ -522,7 +522,7 @@
fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
fun choose v th th' = case concl_of th of
- @{term Trueprop} $ (Const(@{const_name "Ex"},_)$_) =>
+ @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
let
val p = (funpow 2 Thm.dest_arg o cprop_of) th
val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
@@ -926,9 +926,9 @@
Const (@{const_name "op ="}, T) $ _ $ _ =>
if domain_type T = HOLogic.boolT then find_args bounds tm
else dest_arg tm
- | Const (@{const_name "Not"}, _) $ _ => find_term bounds (dest_arg tm)
- | Const (@{const_name "All"}, _) $ _ => find_body bounds (dest_arg tm)
- | Const (@{const_name "Ex"}, _) $ _ => find_body bounds (dest_arg tm)
+ | Const (@{const_name Not}, _) $ _ => find_term bounds (dest_arg tm)
+ | Const (@{const_name All}, _) $ _ => find_body bounds (dest_arg tm)
+ | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
| Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
| Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
--- a/src/HOL/Tools/lin_arith.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Aug 19 16:08:59 2010 +0200
@@ -46,12 +46,12 @@
val mk_Trueprop = HOLogic.mk_Trueprop;
fun atomize thm = case Thm.prop_of thm of
- Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
-fun neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
- | neg_prop ((TP as Const(@{const_name "Trueprop"}, _)) $ t) = TP $ (HOLogic.Not $t)
+fun neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
+ | neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ t) = TP $ (HOLogic.Not $t)
| neg_prop t = raise TERM ("neg_prop", [t]);
fun is_False thm =
@@ -258,10 +258,10 @@
| negate NONE = NONE;
fun decomp_negation data
- ((Const (@{const_name "Trueprop"}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
+ ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
decomp_typecheck data (T, (rel, lhs, rhs))
- | decomp_negation data ((Const (@{const_name "Trueprop"}, _)) $
- (Const (@{const_name "Not"}, _) $ (Const (rel, T) $ lhs $ rhs))) =
+ | decomp_negation data ((Const (@{const_name Trueprop}, _)) $
+ (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
negate (decomp_typecheck data (T, (rel, lhs, rhs)))
| decomp_negation data _ =
NONE;
@@ -273,7 +273,7 @@
in decomp_negation (thy, discrete, inj_consts) end;
fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
- | domain_is_nat (_ $ (Const (@{const_name "Not"}, _) $ (Const (_, T) $ _ $ _))) = nT T
+ | domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
| domain_is_nat _ = false;
@@ -659,7 +659,7 @@
fun negated_term_occurs_positively (terms : term list) : bool =
List.exists
- (fn (Trueprop $ (Const (@{const_name "Not"}, _) $ t)) =>
+ (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
member Pattern.aeconv terms (Trueprop $ t)
| _ => false)
terms;
--- a/src/HOL/Tools/prop_logic.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/prop_logic.ML Thu Aug 19 16:08:59 2010 +0200
@@ -391,11 +391,11 @@
next_idx_is_valid := true;
Unsynchronized.inc next_idx
)
- fun aux (Const (@{const_name "True"}, _)) table =
+ fun aux (Const (@{const_name True}, _)) table =
(True, table)
- | aux (Const (@{const_name "False"}, _)) table =
+ | aux (Const (@{const_name False}, _)) table =
(False, table)
- | aux (Const (@{const_name "Not"}, _) $ x) table =
+ | aux (Const (@{const_name Not}, _) $ x) table =
apfst Not (aux x table)
| aux (Const (@{const_name "op |"}, _) $ x $ y) table =
let
--- a/src/HOL/Tools/sat_funcs.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Thu Aug 19 16:08:59 2010 +0200
@@ -217,7 +217,7 @@
(* Thm.cterm -> int option *)
fun index_of_literal chyp = (
case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
- (Const (@{const_name "Not"}, _) $ atom) =>
+ (Const (@{const_name Not}, _) $ atom) =>
SOME (~ (the (Termtab.lookup atom_table atom)))
| atom =>
SOME (the (Termtab.lookup atom_table atom))
--- a/src/HOL/Tools/simpdata.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML Thu Aug 19 16:08:59 2010 +0200
@@ -45,7 +45,7 @@
(*expects Trueprop if not == *)
of Const (@{const_name "=="},_) $ _ $ _ => th
| _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
- | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
+ | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI}
| _ => th RS @{thm Eq_TrueI}
fun mk_eq_True (_: simpset) r =
--- a/src/HOL/ex/SVC_Oracle.thy Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Thu Aug 19 16:08:59 2010 +0200
@@ -91,15 +91,15 @@
and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
| fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const(@{const_name "Not"}, _)) $ p) = c $ (fm p)
- | fm ((c as Const(@{const_name "True"}, _))) = c
- | fm ((c as Const(@{const_name "False"}, _))) = c
+ | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
+ | fm ((c as Const(@{const_name True}, _))) = c
+ | fm ((c as Const(@{const_name False}, _))) = c
| fm (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
- fun mt ((c as Const(@{const_name "Trueprop"}, _)) $ p) = c $ (fm p)
+ fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
| mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
| mt t = fm t (*it might be a formula*)
in (list_all (params, mt body), !pairs) end;
--- a/src/HOL/ex/svc_funcs.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML Thu Aug 19 16:08:59 2010 +0200
@@ -92,9 +92,9 @@
Const(@{const_name "op &"}, _) => apply c (map tag ts)
| Const(@{const_name "op |"}, _) => apply c (map tag ts)
| Const(@{const_name "op -->"}, _) => apply c (map tag ts)
- | Const(@{const_name "Not"}, _) => apply c (map tag ts)
- | Const(@{const_name "True"}, _) => (c, false)
- | Const(@{const_name "False"}, _) => (c, false)
+ | Const(@{const_name Not}, _) => apply c (map tag ts)
+ | Const(@{const_name True}, _) => (c, false)
+ | Const(@{const_name False}, _) => (c, false)
| Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
if T = HOLogic.boolT then
(*biconditional: with int/nat comparisons below?*)
@@ -189,10 +189,10 @@
Buildin("OR", [fm pos p, fm pos q])
| fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
Buildin("=>", [fm (not pos) p, fm pos q])
- | fm pos (Const(@{const_name "Not"}, _) $ p) =
+ | fm pos (Const(@{const_name Not}, _) $ p) =
Buildin("NOT", [fm (not pos) p])
- | fm pos (Const(@{const_name "True"}, _)) = TrueExpr
- | fm pos (Const(@{const_name "False"}, _)) = FalseExpr
+ | fm pos (Const(@{const_name True}, _)) = TrueExpr
+ | fm pos (Const(@{const_name False}, _)) = FalseExpr
| fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
(*polarity doesn't matter*)
Buildin("=", [fm pos p, fm pos q])
@@ -225,7 +225,7 @@
else fail t
| fm pos t = var(t,[]);
(*entry point, and translation of a meta-formula*)
- fun mt pos ((c as Const(@{const_name "Trueprop"}, _)) $ p) = fm pos (iff_tag p)
+ fun mt pos ((c as Const(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
| mt pos ((c as Const("==>", _)) $ p $ q) =
Buildin("=>", [mt (not pos) p, mt pos q])
| mt pos t = fm pos (iff_tag t) (*it might be a formula*)