[Isarmathlib-devel] ? about Isabelle/Library of Formallized Mathematics

[clefort]

Hello,

I am concerned that when I am creating some script in Isabelle/Isar  
do I need to be in Isabelle/ZF or will the Mathematics library  
execute in Isabelle/Isar?

As I mentioned in my last post I had trouble passing one of your  
first lemmas in Isabelle/Isar.

Thanks

Clinton R. LeFort