Fri, 07 Mar 2014 16:00:45 +0100 | wenzelm | tuned message: reveal ambiguity where Syntax_Phases.decode_term fails and thus reduces proper_results beforehand, e.g. term "f(x := y)" in ~~/src/HOL/Hoare/Hoare_Logic.thy; | changeset | files |
Fri, 07 Mar 2014 15:16:08 +0100 | wenzelm | tuned description and its rendering; | changeset | files |