HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax
fixities. I don't think HOL Light supports comments at this level. HOL4 does,
using SML's (* ... *). So, if you want to write the escaped *, you have to use
our older syntax for the same (using a $ for "op": $*), or
On 1 Jul 2015, at 00:57, Makarius makar...@sketis.net wrote:
On Tue, 30 Jun 2015, Larry Paulson wrote:
It is interesting to look at competing systems and note that every one of
them appears to be fully committed to a plain ASCII syntax as the only way
of writing a formula. I think it may
I'm based off RC0 (at 9e0c62d of the *git* mirror at github.com/seL4/isabelle;
this is tagged Isabelle2014-RC0 and certainly seems to be the same as
251ef0202e71 in the Mercurial world).
I am running code that seemed to be legitimate in 2013-2, but which is now
giving me errors such as
***
I already have the patch you sent me offline in my history.
I will examine the remaining uses of theory_of and see if they're legitimate.
Thanks,
Michael
On 25/08/14 17:32, Lars Noschinski wrote:
On 25.08.2014 09:04, Michael Norrish wrote:
I'm based off RC0 (at 9e0c62d of the *git* mirror
the regression tests for this package need improving, or are uses such as the
above sometimes alright after all?
Best,
Michael
On 26/08/14 13:12, Michael Norrish wrote:
I already have the patch you sent me offline in my history.
I will examine the remaining uses of theory_of and see if they're
This is my experience as well.
Michael
On 19 Dec 2013, at 8:23, Gerwin Klein gerwin.kl...@nicta.com.au wrote:
I have it installed and it's nice for browsing through history, but for
normal daily operation I still find myself using primarily the command line,
mostly because it's quick and
There is not yet a version of the C parser for Isabelle 2013, but there will be
soon.
Michael
On 26/03/2013, at 4:01, Lars Noschinski nosch...@in.tum.de wrote:
On 25.03.2013 17:21, Makarius wrote:
On Mon, 11 Mar 2013, Lars Noschinski wrote:
Indeed and I'm in happy situation that I'm able
On 18/04/12 1:46 PM, Thomas Sewell wrote:
This is used in our modified version of the Schirmer Hoare VCG. I
suppose that we've released the c-parser sources (which load extra
fold_congs) but not the modified Hoare package (which uses them). The
point is to avoid an exponential time/space
On 26/08/11 7:26 AM, Florian Haftmann wrote:
Hi Andreas,
Let me ask something stupid:
why exactly do you guys axiomatize 'a set?
Sure it's admissable and all, but why not do this definitionally
via the obvious typedef?
the answer is rather technical: »typedef« in its current
On 7/01/11 8:05 PM, Alexander Krauss wrote:
But then we need a Marketing division to come up with a new name every 8
months :-}. Year numbers are very comfortable.
You either come up with a set of names to use, or just do what most
software projects do (commercial and open source both), and
Makarius wrote:
On Thu, 12 Nov 2009, Lucas Dixon wrote:
this is interesting to me: I don't understand why you couldn't just
use the -- and ALL of HOL to do exactly what == and !! are doing?
Isn't that what SPL by Zammit did? The dependencies (in Isabelle,
stored in hyps) can all be recorded
Tjark Weber wrote:
But of course a bug tracker is just a tool; in the end its people who
have to work with (or without) it. HOL4's bug tracker (which is
provided by SourceFourge) is not exactly a blazing success either.
Indeed. We only really use it for collecting bugs from users who aren't
12 matches
Mail list logo
