--- a/src/HOL/Import/HOL4Compat.thy Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Import/HOL4Compat.thy Sat Sep 03 15:09:51 2011 -0700
@@ -421,16 +421,6 @@
assume allx': "ALL x. P x \<longrightarrow> x < z"
have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
proof (rule posreal_complete)
- show "ALL x : Collect P. 0 < x"
- proof safe
- fix x
- assume P: "P x"
- from allx
- have "P x \<longrightarrow> 0 < x"
- ..
- with P show "0 < x" by simp
- qed
- next
from px
show "EX x. x : Collect P"
by auto
--- a/src/HOL/Nominal/nominal_datatype.ML Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Sep 03 15:09:51 2011 -0700
@@ -1205,7 +1205,7 @@
val ind_prems' =
map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
- (List.last (binder_types T) --> HOLogic.boolT) -->
+ Term.range_type T -->
HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
--- a/src/HOL/Nominal/nominal_permeq.ML Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Sat Sep 03 15:09:51 2011 -0700
@@ -303,7 +303,7 @@
vs HOLogic.unit;
val s' = list_abs (ps,
Const ("Nominal.supp", fastype_of1 (Ts, s) -->
- List.last (binder_types T) --> HOLogic.boolT) $ s);
+ Term.range_type T) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (prems_of supports_rule'));
--- a/src/HOL/RComplete.thy Sat Sep 03 23:38:06 2011 +0200
+++ b/src/HOL/RComplete.thy Sat Sep 03 15:09:51 2011 -0700
@@ -33,8 +33,8 @@
text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}
lemma posreal_complete:
- assumes positive_P: "\<forall>x \<in> P. (0::real) < x"
- and not_empty_P: "\<exists>x. x \<in> P"
+ fixes P :: "real set"
+ assumes not_empty_P: "\<exists>x. x \<in> P"
and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
proof -