# HG changeset patch
# User wenzelm
# Date 1398700203 -7200
# Node ID 9c3f0ae9953226bbfa6272ebfeaee57a7a4ad38d
# Parent  309e1a61ee7c91928366dffb58a5278c6b604af5
tuned;

diff -r 309e1a61ee7c -r 9c3f0ae99532 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Mon Apr 28 17:48:59 2014 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Mon Apr 28 17:50:03 2014 +0200
@@ -615,19 +615,18 @@
 begin
 
 definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
-  "inf_enat \<equiv> min"
+  "inf_enat = min"
 
 definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
-  "sup_enat \<equiv> max"
+  "sup_enat = max"
 
 definition Inf_enat :: "enat set \<Rightarrow> enat" where
-  "Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
+  "Inf_enat A = (if A = {} then \<infinity> else (LEAST x. x \<in> A))"
 
 definition Sup_enat :: "enat set \<Rightarrow> enat" where
-  "Sup_enat A \<equiv> if A = {} then 0
-    else if finite A then Max A
-                     else \<infinity>"
-instance proof
+  "Sup_enat A = (if A = {} then 0 else if finite A then Max A else \<infinity>)"
+instance
+proof
   fix x :: "enat" and A :: "enat set"
   { assume "x \<in> A" then show "Inf A \<le> x"
       unfolding Inf_enat_def by (auto intro: Least_le) }
diff -r 309e1a61ee7c -r 9c3f0ae99532 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Apr 28 17:48:59 2014 +0200
+++ b/src/HOL/Library/Float.thy	Mon Apr 28 17:50:03 2014 +0200
@@ -919,7 +919,7 @@
   show ?thesis
   proof (cases "0 \<le> l")
     assume "0 \<le> l"
-    def x' == "x * 2 ^ nat l"
+    def x' \<equiv> "x * 2 ^ nat l"
     have "int x * 2 ^ nat l = x'" by (simp add: x'_def int_mult int_power)
     moreover have "real x * 2 powr real l = real x'"
       by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def)
@@ -931,7 +931,7 @@
          (simp add: floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0 round_up_def)
    next
     assume "\<not> 0 \<le> l"
-    def y' == "y * 2 ^ nat (- l)"
+    def y' \<equiv> "y * 2 ^ nat (- l)"
     from `y \<noteq> 0` have "y' \<noteq> 0" by (simp add: y'_def)
     have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
     moreover have "real x * real (2::int) powr real l / real y = x / real y'"
@@ -959,9 +959,12 @@
     using assms by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
 qed
 
-lemma power_aux: assumes "x > 0" shows "(2::int) ^ nat (x - 1) \<le> 2 ^ nat x - 1"
+lemma power_aux:
+  assumes "x > 0"
+  shows "(2::int) ^ nat (x - 1) \<le> 2 ^ nat x - 1"
 proof -
-  def y \<equiv> "nat (x - 1)" moreover
+  def y \<equiv> "nat (x - 1)"
+  moreover
   have "(2::int) ^ y \<le> (2 ^ (y + 1)) - 1" by simp
   ultimately show ?thesis using assms by simp
 qed
@@ -1103,8 +1106,8 @@
 
 lemma lapprox_rat_nonneg:
   fixes n x y
-  defines "p == int n - ((bitlen \<bar>x\<bar>) - (bitlen \<bar>y\<bar>))"
-  assumes "0 \<le> x" "0 < y"
+  defines "p \<equiv> int n - ((bitlen \<bar>x\<bar>) - (bitlen \<bar>y\<bar>))"
+  assumes "0 \<le> x" and "0 < y"
   shows "0 \<le> real (lapprox_rat n x y)"
 using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
    powr_int[of 2, simplified]
diff -r 309e1a61ee7c -r 9c3f0ae99532 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Apr 28 17:48:59 2014 +0200
+++ b/src/HOL/Library/FuncSet.thy	Mon Apr 28 17:50:03 2014 +0200
@@ -23,7 +23,7 @@
 abbreviation
   funcset :: "['a set, 'b set] => ('a => 'b) set"
     (infixr "->" 60) where
-  "A -> B == Pi A (%_. B)"
+  "A -> B \<equiv> Pi A (%_. B)"
 
 notation (xsymbols)
   funcset  (infixr "\<rightarrow>" 60)
@@ -41,8 +41,8 @@
   "_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
 
 translations
-  "PI x:A. B" == "CONST Pi A (%x. B)"
-  "%x:A. f" == "CONST restrict (%x. f) A"
+  "PI x:A. B" \<rightleftharpoons> "CONST Pi A (%x. B)"
+  "%x:A. f" \<rightleftharpoons> "CONST restrict (%x. f) A"
 
 definition
   "compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" where
@@ -352,7 +352,7 @@
 
 syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
 
-translations "PIE x:A. B" == "CONST Pi\<^sub>E A (%x. B)"
+translations "PIE x:A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (%x. B)"
 
 abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60) where
   "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"