Hello everyone,
Recently I noticed that in HOLCF, whenever I do a theorem search for
theorems containing the constant UU (i.e. bottom), the search fails
with an UnequalLengths exception. I tracked the problem down to this
specific theorem from Fun_Cpo.thy: Before this point, find_theorems
UU
That is certainly my change, but I don't understand why preventing
self-referential type instantiations should affect the find_theorems function.
Can you get a full trace back from the exception?
Larry
On 18 Nov 2010, at 16:03, Brian Huffman wrote:
Hello everyone,
Recently I noticed that
On Thu, Nov 18, 2010 at 8:25 AM, Lawrence Paulson l...@cam.ac.uk wrote:
That is certainly my change, but I don't understand why preventing
self-referential type instantiations should affect the find_theorems
function. Can you get a full trace back from the exception?
Here's what I get from
The effect of my change typedef (open) unit is to remove the
definition of the following constant
unit_def: unit == {True}
thus making the name unit available to users.
- Brian
On Thu, Nov 18, 2010 at 1:58 PM, Makarius makar...@sketis.net wrote:
Hi Brian,
can you say a few words about
On Thu, Nov 18, 2010 at 2:59 PM, Makarius makar...@sketis.net wrote:
On Thu, 18 Nov 2010, Brian Huffman wrote:
The effect of my change typedef (open) unit is to remove the
definition of the following constant
unit_def: unit == {True}
thus making the name unit available to users.
So this
Makarius wrote:
Here are some examples for the isabelle scala toplevel:
[...]
Thanks, these are good pointers.
Unfortunately, this is (once again) harder than I thought. Here are the
issues/questions:
- Relative paths are not resolved by the current simple parser. I
remember that there used
On Thu, Nov 18, 2010 at 1:58 PM, Makarius makar...@sketis.net wrote:
For some reason, many people have started to sequeze everything in a single
line (frequent), or imitate the headline/body text format of other projects
with a completely different structure (rare). The reason might be as
