55 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
55 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
56 interface instead. |
56 interface instead. |
57 |
57 |
58 |
58 |
59 *** Pure *** |
59 *** Pure *** |
|
60 |
|
61 * Module moves in repository: |
|
62 src/Pure/Tools/value.ML ~> src/Tools/ |
|
63 src/Pure/Tools/quickcheck.ML ~> src/Tools/ |
60 |
64 |
61 * Slightly more coherent Pure syntax, with updated documentation in |
65 * Slightly more coherent Pure syntax, with updated documentation in |
62 isar-ref manual. Removed locales meta_term_syntax and |
66 isar-ref manual. Removed locales meta_term_syntax and |
63 meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, |
67 meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, |
64 INCOMPATIBILITY in rare situations. |
68 INCOMPATIBILITY in rare situations. |
130 demanding keyword 'by' and supporting the full method expression |
134 demanding keyword 'by' and supporting the full method expression |
131 syntax just like the Isar command 'by'. |
135 syntax just like the Isar command 'by'. |
132 |
136 |
133 |
137 |
134 *** HOL *** |
138 *** HOL *** |
|
139 |
|
140 * Made repository layout more coherent with logical |
|
141 distribution structure: |
|
142 |
|
143 src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy |
|
144 src/HOL/Library/Code_Message.thy ~> src/HOL/ |
|
145 src/HOL/Library/GCD.thy ~> src/HOL/ |
|
146 src/HOL/Library/Order_Relation.thy ~> src/HOL/ |
|
147 src/HOL/Library/Parity.thy ~> src/HOL/ |
|
148 src/HOL/Library/Univ_Poly.thy ~> src/HOL/ |
|
149 src/HOL/Real/ContNotDenum.thy ~> src/HOL/ |
|
150 src/HOL/Real/Lubs.thy ~> src/HOL/ |
|
151 src/HOL/Real/PReal.thy ~> src/HOL/ |
|
152 src/HOL/Real/Rational.thy ~> src/HOL/ |
|
153 src/HOL/Real/RComplete.thy ~> src/HOL/ |
|
154 src/HOL/Real/RealDef.thy ~> src/HOL/ |
|
155 src/HOL/Real/RealPow.thy ~> src/HOL/ |
|
156 src/HOL/Real/Real.thy ~> src/HOL/ |
|
157 src/HOL/Complex/Complex_Main.thy ~> src/HOL/ |
|
158 src/HOL/Complex/Complex.thy ~> src/HOL/ |
|
159 src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/ |
|
160 src/HOL/Hyperreal/Deriv.thy ~> src/HOL/ |
|
161 src/HOL/Hyperreal/Fact.thy ~> src/HOL/ |
|
162 src/HOL/Hyperreal/Integration.thy ~> src/HOL/ |
|
163 src/HOL/Hyperreal/Lim.thy ~> src/HOL/ |
|
164 src/HOL/Hyperreal/Ln.thy ~> src/HOL/ |
|
165 src/HOL/Hyperreal/Log.thy ~> src/HOL/ |
|
166 src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/ |
|
167 src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/ |
|
168 src/HOL/Hyperreal/Series.thy ~> src/HOL/ |
|
169 src/HOL/Hyperreal/Taylor.thy ~> src/HOL/ |
|
170 src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/ |
|
171 src/HOL/Real/Float ~> src/HOL/Library/ |
|
172 |
|
173 src/HOL/arith_data.ML ~> src/HOL/Tools |
|
174 src/HOL/hologic.ML ~> src/HOL/Tools |
|
175 src/HOL/simpdata.ML ~> src/HOL/Tools |
|
176 src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML |
|
177 src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools |
|
178 src/HOL/nat_simprocs.ML ~> src/HOL/Tools |
|
179 src/HOL/Real/float_arith.ML ~> src/HOL/Tools |
|
180 src/HOL/Real/float_syntax.ML ~> src/HOL/Tools |
|
181 src/HOL/Real/rat_arith.ML ~> src/HOL/Tools |
|
182 src/HOL/Real/real_arith.ML ~> src/HOL/Tools |
135 |
183 |
136 * If methods "eval" and "evaluation" encounter a structured proof state |
184 * If methods "eval" and "evaluation" encounter a structured proof state |
137 with !!/==>, only the conclusion is evaluated to True (if possible), |
185 with !!/==>, only the conclusion is evaluated to True (if possible), |
138 avoiding strange error messages. |
186 avoiding strange error messages. |
139 |
187 |