src/HOL/IsaMakefile

 ## HOL-Hyperreal
 
 HOL-Hyperreal: HOL-Real $(OUT)/HOL-Hyperreal
 
 $(OUT)/HOL-Hyperreal: $(OUT)/HOL-Real Hyperreal/ROOT.ML\
+  Library/Zorn.thy\
   Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
   Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
   Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
   Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
   Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\

   Hyperreal/NSA.ML Hyperreal/NSA.thy\
   Hyperreal/NthRoot.ML Hyperreal/NthRoot.thy\
   Hyperreal/Poly.ML Hyperreal/Poly.thy\
   Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\
   Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\
-  Hyperreal/Transcendental.thy Hyperreal/Zorn.ML Hyperreal/Zorn.thy\
-  Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
+  Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
   Hyperreal/hypreal_arith0.ML
 	@cd Hyperreal; $(ISATOOL) usedir -b $(OUT)/HOL-Real HOL-Hyperreal
 
 
 ## HOL-Hyperreal-ex

   Library/Permutation.thy Library/Primes.thy \
   Library/Quotient.thy Library/Ring_and_Field.thy \
   Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
   Library/README.html Library/Continuity.thy \
   Library/Nested_Environment.thy Library/Rational_Numbers.thy \
+  Library/Zorn.thy\
   Library/Library/ROOT.ML Library/Library/document/root.tex \
   Library/Library/document/root.bib Library/While_Combinator.thy
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library