--- a/src/HOL/Library/positivstellensatz.ML Wed Dec 20 18:51:13 2017 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Wed Dec 20 22:07:05 2017 +0100
@@ -370,8 +370,8 @@
fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
fun oprconv cv ct =
let val g = Thm.dest_fun2 ct
- in if g aconvc @{cterm "op <= :: real => _"}
- orelse g aconvc @{cterm "op < :: real => _"}
+ in if g aconvc @{cterm "(op <=) :: real => _"}
+ orelse g aconvc @{cterm "(op <) :: real => _"}
then arg_conv cv ct else arg1_conv cv ct
end
@@ -406,13 +406,13 @@
| Axiom_le n => nth les n
| Axiom_lt n => nth lts n
| Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop}
- (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x))
+ (Thm.apply (Thm.apply @{cterm "(op =)::real => _"} (mk_numeric x))
@{cterm "0::real"})))
| Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop}
- (Thm.apply (Thm.apply @{cterm "op <=::real => _"}
+ (Thm.apply (Thm.apply @{cterm "(op <=)::real => _"}
@{cterm "0::real"}) (mk_numeric x))))
| Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop}
- (Thm.apply (Thm.apply @{cterm "op <::real => _"} @{cterm "0::real"})
+ (Thm.apply (Thm.apply @{cterm "(op <)::real => _"} @{cterm "0::real"})
(mk_numeric x))))
| Square pt => square_rule (cterm_of_poly pt)
| Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
@@ -428,9 +428,9 @@
val concl = Thm.dest_arg o Thm.cprop_of
fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
- val is_req = is_binop @{cterm "op =:: real => _"}
- val is_ge = is_binop @{cterm "op <=:: real => _"}
- val is_gt = is_binop @{cterm "op <:: real => _"}
+ val is_req = is_binop @{cterm "(op =):: real => _"}
+ val is_ge = is_binop @{cterm "(op <=):: real => _"}
+ val is_gt = is_binop @{cterm "(op <):: real => _"}
val is_conj = is_binop @{cterm HOL.conj}
val is_disj = is_binop @{cterm HOL.disj}
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
@@ -476,7 +476,7 @@
fun dest_binary b ct =
if is_binop b ct then Thm.dest_binop ct
else raise CTERM ("dest_binary",[b,ct])
- val dest_eq = dest_binary @{cterm "op = :: real => _"}
+ val dest_eq = dest_binary @{cterm "(op =) :: real => _"}
val neq_th = nth pth 5
fun real_not_eq_conv ct =
let
@@ -486,8 +486,8 @@
val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
val th' = Drule.binop_cong_rule @{cterm HOL.disj}
- (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
- (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
+ (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_p)
+ (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_n)
in Thm.transitive th th'
end
fun equal_implies_1_rule PQ =
--- a/src/HOL/Lifting.thy Wed Dec 20 18:51:13 2017 +0100
+++ b/src/HOL/Lifting.thy Wed Dec 20 22:07:05 2017 +0100
@@ -228,7 +228,7 @@
fixes Abs :: "'a \<Rightarrow> 'b"
and Rep :: "'b \<Rightarrow> 'a"
assumes "type_definition Rep Abs (UNIV::'a set)"
- shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
+ shows "equivp (op= ::'a\<Rightarrow>'a\<Rightarrow>bool)"
by (rule identity_equivp)
lemma typedef_to_Quotient:
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 20 18:51:13 2017 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 20 22:07:05 2017 +0100
@@ -1796,7 +1796,7 @@
else if lam_trans = combs_or_liftingN then
lift_lams_part_1 ctxt type_enc
##> map (fn t => (case head_of (strip_qnt_body @{const_name All} t) of
- @{term "op =::bool => bool => bool"} => t
+ @{term "op = ::bool => bool => bool"} => t
| _ => introduce_combinators ctxt (intentionalize_def t)))
#> lift_lams_part_2 ctxt
else if lam_trans = keep_lamsN then
--- a/src/HOL/Tools/groebner.ML Wed Dec 20 18:51:13 2017 +0100
+++ b/src/HOL/Tools/groebner.ML Wed Dec 20 22:07:05 2017 +0100
@@ -899,7 +899,7 @@
| Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
| Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
| Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
- | \<^term>\<open>op \<Longrightarrow>\<close> $_$_ => find_args bounds tm
+ | \<^term>\<open>Pure.imp\<close> $_$_ => find_args bounds tm
| Const("op ==",_)$_$_ => find_args bounds tm (* FIXME proper const name *)
| \<^term>\<open>Trueprop\<close>$_ => find_term bounds (Thm.dest_arg tm)
| _ => raise TERM ("find_term", []))
--- a/src/HOL/Topological_Spaces.thy Wed Dec 20 18:51:13 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Wed Dec 20 22:07:05 2017 +0100
@@ -2158,11 +2158,11 @@
lemma compactE_image:
assumes "compact S"
- and op: "\<And>T. T \<in> C \<Longrightarrow> open (f T)"
+ and opn: "\<And>T. T \<in> C \<Longrightarrow> open (f T)"
and S: "S \<subseteq> (\<Union>c\<in>C. f c)"
obtains C' where "C' \<subseteq> C" and "finite C'" and "S \<subseteq> (\<Union>c\<in>C'. f c)"
apply (rule compactE[OF \<open>compact S\<close> S])
- using op apply force
+ using opn apply force
by (metis finite_subset_image)
lemma compact_Int_closed [intro]: