On 17.05.2013 17:24, Makarius wrote:
On Thu, 16 May 2013, Lars Noschinski wrote:
-
ML_PLATFORM=x86-linux
ML_HOME=/home/polyml/polyml-svn/x86-linux
ML_SYSTEM=polyml-5.5.0
ML_OPTIONS=-H 1000
ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2
On 21.05.2013 13:59, Makarius wrote:
I do this usually by searching backwards for context (which means I
might miss contexts opened by locale) or manually search through the
sidekick. To check whether I am in a local context at all, I usually
insert an additional end command and look for an
On 23.04.2013 19:37, Florian Haftmann wrote:
See now http://isabelle.in.tum.de/repos/isabelle/rev/e4b5bebe5235.
This does not seem to work for me in 06db08182c4b:
-
theory Interpretation imports Main begin
locale A begin
definition f ::
Hallo,
i want to create a datatype that allows me to write functions from a nat subset
to another nat subset.
for example i wanna be able to write:
definition f: {1,2,3} = {4,5}
1 --4, 2--4, 3--5
or another one:
definition g : {6,8} = {2,3,4}
Hallo,
partial function in Isabelle are usually modelled as 'a ⇀ 'b, which is
an abbreviation for 'a ⇒ 'b option. There is syntax such as [1 ↦ 2, 3 ↦
4], meaning, basically, λx. if x = 1 then Some 2 else if x = 3 then
Some 4 else None. There is also update syntax for such function, such
as f(1 ↦
Hello,
how can i prove the following:
( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A} ) ={c1, c2,
c3} ?
Thank you!___
isabelle-dev mailing list
isabelle-...@in.tum.de
On 22.05.2013 17:14, Roger H. wrote:
how can i prove the following:
( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A} ) = {c1, c2, c3} ?
This is a topic for the isabelle-users mailing list; this mailing list
is for topics specific to the developer version of Isabelle.
But the answer is: You
Quoting Lars Noschinski nosch...@in.tum.de:
How is interpretation related to print_context? It seems that
neither interpret nor interpretation extends the context as
displayed by print_context?
I don't know the answer to that, but for a particular locale x you
should be able to find all
