Am 02.11.2010 um 17:30 schrieb Makarius: > Now (e.g. in version c753e3f8b4d6) you can use Parse.real to get the result > of the user using either integer or float notation. The Attrib.config_real > also does that internally.
Great. Then I'm totally sold. :) Jasmin _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
