Why do we need abbreviations such as these?
abbreviation real_of_nat :: nat \Rightarrow real”
where real_of_nat \equiv of_nat
abbreviation real_of_int :: int \Rightarrow real”
where real_of_int \equiv of_int
abbreviation real_of_rat :: rat \Rightarrow real”
where real_of_rat
Hi Manuel,
I also vote for b). I would also like to add that I ran into situations
where I required the notation of an inverse element in a ring. I defined
this as ring_inv x = 1 div x. For instance, on int, we have ring_inv
1 = 1 and ring_inv (-1) = -1 and everything else is basically
Hi again,
after I first iteration of discussion I see a list of three requirements:
1. Conversions can be written succinctly.
2. Conversions are printed succinctly.
3. Conversions are unique, there are no accidental equivalences which
require explicit conversions.
Concerning (1), my guess
Cleaning up some obscure corners of the system, I've come across the old
defer_recdef command.
Are there any remaining uses of this historical relic? I don't see any
in the main Isabelle repository + AFP.
Some years ago the idea was to let recdef stand as long as there are
examples in the
Maybe we should resurrect the idea of using adhoc overloading for the
real abbreviation.
The idea in itself is not bad, but I am reluctant to pull ad-hoc
overloading into the HOL theories itself. There are still too many
dragons sitting in the dark.
Florian, does your rework of the generic
On 5 Jun 2015, at 22:22, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Why do we need abbreviations such as these?
abbreviation real_of_nat :: nat \Rightarrow real”
where real_of_nat \equiv of_nat
abbreviation real_of_int :: int \Rightarrow real”
where
I’d be happy to see the complete phasing out of TFL. It’s had its day. It was
always a tricky thing to maintain. I’m amazed that it still works despite all
of the many fundamental changes to system APIs.
Larry
On 5 Jun 2015, at 21:42, Florian Haftmann
