--- a/NEWS Mon Nov 25 20:25:22 2013 +0100
+++ b/NEWS Tue Nov 26 15:54:03 2013 +0100
@@ -37,6 +37,8 @@
* Elimination of fact duplicates:
equals_zero_I ~> minus_unique
diff_eq_0_iff_eq ~> right_minus_eq
+ nat_infinite ~> infinite_UNIV_nat
+ int_infinite ~> infinite_UNIV_int
INCOMPATIBILITY.
* Fact name consolidation:
--- a/src/HOL/Library/Library.thy Mon Nov 25 20:25:22 2013 +0100
+++ b/src/HOL/Library/Library.thy Tue Nov 26 15:54:03 2013 +0100
@@ -65,6 +65,7 @@
Transitive_Closure_Table
Wfrec
While_Combinator
+ Zorn
begin
end
(*>*)
--- a/src/Tools/subtyping.ML Mon Nov 25 20:25:22 2013 +0100
+++ b/src/Tools/subtyping.ML Tue Nov 26 15:54:03 2013 +0100
@@ -129,7 +129,8 @@
infixr ++> +@> (* lazy error msg composition *)
-fun err ++> prt = err #> apsnd (cons prt);
+fun (err : unit -> string * Pretty.T list) ++> (prt : Pretty.T) =
+ err #> apsnd (cons prt);
val op +@> = Library.foldl op ++>;
fun eval_err err = err ()