--- a/src/HOL/Library/Extended_Real.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Mon Jul 06 22:57:34 2015 +0200
@@ -257,7 +257,7 @@
| "real_ereal \<infinity> = 0"
| "real_ereal (-\<infinity>) = 0"
by (auto intro: ereal_cases)
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
instance ..
end
@@ -340,7 +340,7 @@
with prems show P
by (cases rule: ereal2_cases[of a b]) auto
qed auto
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
lemma Infty_neq_0[simp]:
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
@@ -509,7 +509,7 @@
using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
instance ereal :: dense_linorder
- by default (blast dest: ereal_dense2)
+ by standard (blast dest: ereal_dense2)
instance ereal :: ordered_ab_semigroup_add
proof
@@ -848,7 +848,7 @@
| "sgn (\<infinity>::ereal) = 1"
| "sgn (-\<infinity>::ereal) = -1"
by (auto intro: ereal_cases)
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
function times_ereal where
"ereal r * ereal p = ereal (r * p)"
@@ -1602,7 +1602,7 @@
definition [simp]: "sup x y = (max x y :: ereal)"
definition [simp]: "inf x y = (min x y :: ereal)"
-instance by default simp_all
+instance by standard simp_all
end
@@ -1706,7 +1706,7 @@
open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
instance
- by default (simp add: open_ereal_generated)
+ by standard (simp add: open_ereal_generated)
end