Friends and Colleagues,
I'm pleased to announce that on May 2nd I will be joining Flemming
Andersen's formal verification (FV) team within Intel's Many Integrated Core
(MIC) supercomputing division.
The MIC division is developing next-generation supercomputing and cloud
computing
Thanks Makarius, I believe that addresses my use-case.
Another question: If the user asks Isabelle to process theory A, and
theory A has statement
imports dir1/B
and theory B has statement
imports dir2/C
then will Isabelle look for theory C in dir1 or dir1/dir2 ?
In other words, does
A while back Larry made this comment:
I have just remembered that I always advise people to use “auto” prior
to trying sledgehammer, because it will split up the subgoal into
manageable parts and simplify them. This is bad advice if “auto” can
render the problem impossible to prove.
Was it
, Gerwin Klein wrote:
John Matthews wrote:
If I turn on show types in Isabelle_19-Nov-2007 and run the
following commands:
theory WordTest imports WordMain
begin
lemma P (ucast ((0b1110 :: 4 word) 1) :: 2 word)
apply simp
Isabelle displays the simplified subgoal as:
goal (1
Let me add my thanks too, it was a very productive and enjoyable
trip! It's also really encouraging to see all the good Isabelle work
presented at TPHOLs this year. I especially liked one presenter's
comment saying there are only four theorem provers capable of doing
real mathematics, and
