On Thu, 18 Nov 2010, Brian Huffman wrote:
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
On Thu, 18 Nov 2010, Brian Huffman wrote:
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
I will tackle your questions one at a time.
The difficulty with your original question concerns, what do we mean by
higher-order matching? For Isabelle, these are nothing but unifiers which leave
the object unchanged.
The problem is that you are trying to match ?x ?y against ?f ?stuff and
On 19/11/10 12:28, Lawrence Paulson wrote:
Looking at this again, I'm not certain there is a bug. You are displaying the
variable assignments, but are you first applying the type variable assignments?
Both must be used in order to instantiate the object term.
Please bear with me -- I'm not
On Fri, 19 Nov 2010, Tobias Nipkow wrote:
Just for the record: the code eta-expands terms on the fly, but the
presence of beta-redexes may well confuse it.
It is known for many years that the pattern unification does have
occasional problems with beta redexes. This is one of the things that
On 19/11/10 14:10, Lawrence Paulson wrote:
If you look at the file Pure/envir.ML, you will find the definition of
environments (which has separate components for the two assignments) as well as
primitives that you should use to apply an environment to a term. If you only
look at assignments
Indeed I find the code peculiar, in that it delivers the higher-order matchers
followed by the first-order ones. But these are different things. And I imagine
there is often redundancy.
Larry
On 19 Nov 2010, at 15:50, Michael Chan wrote:
On 19/11/10 14:10, Lawrence Paulson wrote:
If you look
On Fri, Nov 19, 2010 at 8:58 AM, Tobias Nipkow nip...@in.tum.de wrote:
I don't understand this: why does latex work for the release version but
not the development version? But indeed, it fails for me too.
I created an extremely simplified version of the Shivers-CFA entry
(building on
On Fri, 19 Nov 2010, Brian Huffman wrote:
http://isabelle.in.tum.de/repos/isabelle/rev/b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste
of Isabelle symbols;
The root.tex of the Shivers-CFA entry contains the following two lines:
\usepackage[normalem]{ulem}
On Fri, 19 Nov 2010, Lawrence Paulson wrote:
Indeed I find the code peculiar, in that it delivers the higher-order
matchers followed by the first-order ones. But these are different
things. And I imagine there is often redundancy.
Unify.matchers started as Isar-specific
On Fri, Nov 19, 2010 at 2:40 PM, Joachim Breitner
m...@joachim-breitner.de wrote:
Hi everyone,
[...]
I’m sorry for the trouble my submission causes. When writing the
theories I had planned to actually use the proof document as my project
report, therefore the trouble I went through to have the
11 matches
Mail list logo
