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

  "~~/src/HOL/Main"

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").

Cheers
Lars




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