equal
deleted
inserted
replaced
139 Real/Complex_Numbers.thy \ |
139 Real/Complex_Numbers.thy \ |
140 Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \ |
140 Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \ |
141 Real/PRat.ML Real/PRat.thy \ |
141 Real/PRat.ML Real/PRat.thy \ |
142 Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \ |
142 Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \ |
143 Real/ROOT.ML Real/Real.thy \ |
143 Real/ROOT.ML Real/Real.thy \ |
144 Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \ |
144 Real/RealArith0.thy Real/real_arith0.ML \ |
145 Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \ |
145 Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \ |
146 Real/RealBin.thy Real/RealDef.thy \ |
146 Real/RealBin.thy Real/RealDef.thy \ |
147 Real/RealInt.thy Real/RealOrd.thy \ |
147 Real/RealInt.thy Real/RealOrd.thy \ |
148 Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\ |
148 Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\ |
149 Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \ |
149 Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \ |