[Isarmathlib-devel] problem loading Isarmath library

[Slawomir Kolodynski]

>What is a simple way to experiment with some of the
lemmas in your isarmath library

I assume you have a working Isabelle installation with
the ZF logic and you have downloaded the latest
version of the library from 

http://download.savannah.nongnu.org/releases/isarmathlib/
  

When you unpack the isarmathlib-1.3.0.tar.gz file it
will create a directory structure. In one of
subdirectories there will be a lot of files with
extension ".thy". Create another file called, say
"test.thy" in that directory. Then run "Isabelle
test.thy &" from that directory. If your Isabelle
installation works as mine (on Ubuntu Linux), this
will call Xemacs with ProofGeneral. 
The first thing you need to do in ProofGeneral is to
switch the logic from the default (which is HOL) to
ZF. ProofGeneral should have a menu tab called
Isabelle. There is a way to change the logic there.   
 

Copy to your file something like

header {*\isaheader{test.thy}*}
theory test imports Topology_ZF

begin

(* state and prove some lemma here *)

end

Of course you can replace Topology_ZF by any other
theory file from IsarMathLib or the standard Isabelle
distribution. 

>Is there a repository of the isarmath newsgroup

There are archives at 

http://lists.gnu.org/archive/html/isarmathlib-devel/

but there is practically nothing there for the simple
reason that I am the only contributor so far.

greetings
Slawek


http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com