On Fri, 2 Aug 2013, Christian Sternagel wrote:
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you feel like making an example theory, e.g.
src/HOL/ex/Adhoc_Overloading_Examples.thy or a short entry for the
isar-ref manual? E.g. somewhere here
http://isabelle.in.tum.de/repos/isabelle/annotate/122416054a9c/src/Doc/IsarRef/HOL_Specific.thy
I gave both a try. Please find the resulting changesets (via "hg export")
attached (I also squeezed in some unrelated changes: spell-checking, tuning
of error messages. I hope that is okay).
The tuning etc. is fine (it looks like done with care).
What is missing in the commit is your new file
src/HOL/ex/Adhoc_Overloading_Examples.thy
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
