Re: [isabelle] folding and linking in jEdit; curry/split

Dear Henning,

> Currently I am working quite a lot on low levels, so I wonder what is
> the best way to have theories like Inductive.thy "linked", that is, when
> clicking on a lemma, I move to that spot?
> I tried setting the base theory to Pure, but then a lot of errors occurred.

you can start Isabelle/jEdit like this:

  isabelle jedit -l Pure

or, as you probably did, change the image from "HOL" to "Pure" in the
Theories panel.

If you then want to use HOL stuff, import from


Then jEdit will load all the theories from HOL for you and you can
Ctrl-Click there as usual.

> On the other hand, regarding the content, I want to show something like
> lemma "{ f::'a => 'b . True } \subseteq (UNIV::('a \times 'b ) set)"

This looks like a type error to me ... You are comparing a set of
functions to a set of tuples.

In any case, your statement is trivial: Every set is a subset of UNIV
(see theorem "Set.subset_UNIV").


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