src/HOL/Analysis/Brouwer_Fixpoint.thy
changeset 68361 20375f232f3b
parent 68296 69d680e94961
child 68617 75129a73aca3
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sat Jun 02 22:57:44 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Jun 03 15:22:30 2018 +0100
     1.3 @@ -40,9 +40,7 @@
     1.4  
     1.5  lemmas swap_apply1 = swap_apply(1)
     1.6  lemmas swap_apply2 = swap_apply(2)
     1.7 -lemmas lessThan_empty_iff = Iio_eq_empty_iff_nat
     1.8  lemmas Zero_notin_Suc = zero_notin_Suc_image
     1.9 -lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
    1.10  
    1.11  lemma pointwise_minimal_pointwise_maximal:
    1.12    fixes s :: "(nat \<Rightarrow> nat) set"