src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
changeset 64267 b9a1486e79be
parent 63562 6f7a9d48a828
child 64911 f0e07600de47
     1.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -402,4 +402,4 @@
     1.4    shows "bourbaki_witt_fixpoint Sup {(x, y). x \<le> y} f"
     1.5  by unfold_locales (auto simp: assms Sup_upper order_on_defs Field_def intro: refl_onI transI antisymI Sup_least)
     1.6  
     1.7 -end
     1.8 \ No newline at end of file
     1.9 +end