equal
deleted
inserted
replaced
233 src/HOL/nat_simprocs.ML ~> src/HOL/Tools |
233 src/HOL/nat_simprocs.ML ~> src/HOL/Tools |
234 src/HOL/Real/float_arith.ML ~> src/HOL/Tools |
234 src/HOL/Real/float_arith.ML ~> src/HOL/Tools |
235 src/HOL/Real/float_syntax.ML ~> src/HOL/Tools |
235 src/HOL/Real/float_syntax.ML ~> src/HOL/Tools |
236 src/HOL/Real/rat_arith.ML ~> src/HOL/Tools |
236 src/HOL/Real/rat_arith.ML ~> src/HOL/Tools |
237 src/HOL/Real/real_arith.ML ~> src/HOL/Tools |
237 src/HOL/Real/real_arith.ML ~> src/HOL/Tools |
|
238 |
|
239 src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL |
|
240 src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL |
|
241 src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL |
|
242 src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL |
|
243 src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL |
|
244 src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL |
238 |
245 |
239 * If methods "eval" and "evaluation" encounter a structured proof state |
246 * If methods "eval" and "evaluation" encounter a structured proof state |
240 with !!/==>, only the conclusion is evaluated to True (if possible), |
247 with !!/==>, only the conclusion is evaluated to True (if possible), |
241 avoiding strange error messages. |
248 avoiding strange error messages. |
242 |
249 |