src/HOL/Library/Zorn.thy
changeset 35175 61255c81da01
parent 32960 69916a850301
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Library/Zorn.thy	Wed Feb 17 10:00:22 2010 -0800
     1.2 +++ b/src/HOL/Library/Zorn.thy	Wed Feb 17 10:30:36 2010 -0800
     1.3 @@ -333,7 +333,7 @@
     1.4  
     1.5  lemma antisym_init_seg_of:
     1.6    "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r=s"
     1.7 -by(auto simp:init_seg_of_def)
     1.8 +unfolding init_seg_of_def by safe
     1.9  
    1.10  lemma Chain_init_seg_of_Union:
    1.11    "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"