Re: [isabelle] Re : I'm a new Isabelle User!

Hi Patrick,

as a convenience, note that usually is it most appropriate to post
generic questions to the isabelle-users at mailing list.

> i'm coming with my mail to you because i have a problem and question
> about Isabelle prover.i've read you books and papers about Isabelle's
> Logic HOL, and old Introduction to Isabelle, but i don't understand :

You should definitely stay away from these two manuals ;-) which are
really outdated;  the definite entrance point to get a little acquainted
with HOL is the "Tutorial on Isabelle/HOL".

> 1- About the installation, i've try to install Isabelle on my computer,
> but it is so difficult to me.It is ask me  "Emacs package" and when i
> install Emacs package, it is look about Emacs version: i don't
> undrestand why and how can i do to have a complete Isabelle's
> installation? the OS on my computer is Ubuntu.

Hmmm... the GNU emacs coming with Ubuntu should be suitable (AFAIK at
least since version 8.04 -- you can find out your version using "less
/etc/issue" on the shell).  A "sudo apt-get install emacs" should do the

> 2- what is proofGeneral? Isawin? and what is their utility on Isabelle
> process?

ProofGeneral is an extension to emacs which provides a simple user
interface to isabelle.  The other possibility is to work on a tty
command line interface; I'm almost sure this is not what you want...

> 3- my next question is about HOL which is using in Isabelle.i don't know
> if HOL is a Theorie or an logic using to developpe theories?

HOL is short for Higher-Order Logic and is one of the calculi the
Isabelle Distribution is equipped with;  it is the most popular and of
Isabelle logics and sometimes even used synonymously, but be aware that
there are other implementations of HOL around.

To answer your question in particular: in Isabelle there is no
difference between theories which "implement" a logic and theories which
"build upon" an implemented logic -- technically they are the same.  As
the tutorial says, for beginners the way to start is to use the existing
precompiled HOL session and base the first development on it:

	theory Foo
	imports Main


> 4-my last preocupation is aboutTactic and Tactical, Goal and Subgoal

Dont't hesitate to ask further questions.

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.