I have redirected your request to isabelle-us...@cl.cam.ac.uk. That is the
appropriate mailing list for users' questions.
The developers' mailing list is for use by the Isabelle developers.
Larry Paulson
On 27 Mar 2012, at 09:14, charmi panchal wrote:
Hello,
I am a beginner of Isabelle and
Hello,
I am trying to use jedit with the Isabelle development version
I have scala-2.9.1-1 and I downloaded jedit_build-20120313.
I set the paths
export
SCALA_HOME=/Users/viorel/Work/isabelle-dev/isabelle/contrib/scala-2.9.1-1
export
Dear all,
trying to import simultaneously the theory file
HOL/Matrix/Matrix.thy and the afp entry
http://afp.sourceforge.net/entries/Matrix.shtml into a file, it seems
that the second theory file unloads the first one (as Makarius
suggested in his mail):
theory Matrix_ex
imports
On Tue, 27 Mar 2012, Viorel Preoteasa wrote:
I am trying to use jedit with the Isabelle development version
I have scala-2.9.1-1 and I downloaded jedit_build-20120313.
I set the paths
export
SCALA_HOME=/Users/viorel/Work/isabelle-dev/isabelle/contrib/scala-2.9.1-1
export
On 3/27/12 11:59 PM, Makarius wrote:
On Tue, 27 Mar 2012, Viorel Preoteasa wrote:
I am trying to use jedit with the Isabelle development version
I have scala-2.9.1-1 and I downloaded jedit_build-20120313.
I set the paths
export
Hi Ondřej,
in
http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53
the name given to the derived theorem is unsatisfactory. Since it is
not a »code-only« theorem, it should not carry the »code« within. If it
would be a »code-only« theorem, the convention is to suffix with
