Time 
Nick 
Message 
01:18 

ertes joined #isabelle 
01:48 

ilbot3 joined #isabelle 
01:48 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
06:17 
ammbauer 
is there a way to find the corresponding term to a symbol? for example I have this expression "(λB. ∫⇧+ M'. emeasure M' B ∂M)". How do I find out what ∫⇧+ or ∂ stand for? 
06:44 
pruvisto 
I usually just do "ML ‹@{term "foo"}›" 
06:45 
pruvisto 
or you can ask your friendly advisor and he'll tell you that "∫⇧+" and "∂" are both part of the syntax for nn_integral :P 
06:47 
pruvisto 
the thing after the ∂ is the measure space that you integrate "over" 
06:47 
pruvisto 
i.e. in the "normal" integral that's usually "lborel", the Lebesgue–Borel measure 
06:47 
pruvisto 
if you choose "count_space A", your integral just corresponds to the sum over all elements in the set A 
06:47 
pruvisto 
nn_integral has the added twist that it "ignores" the negative part of the function 
06:47 
pruvisto 
so "nn_integral f M" is essentially the integral of "max(f, 0)" over the entire space of M 
06:47 
pruvisto 
(The advantage of nn_integral is that it always exists as long as f is measurable, though it may be infinite) 
06:57 
ammbauer 
pruvisto: thanks 
06:57 
ammbauer 
it would be really cool if you could also click on the symbols and jump to the definition 
07:29 

pootler joined #isabelle 
07:31 
pruvisto 
ammbauer: uuh, i think you can 
07:34 

Merv_ left #isabelle 
07:35 

Merv_ joined #isabelle 
07:36 

Merv_ left #isabelle 
07:43 
ammbauer 
pruvisto: not with translations like ∫⇧+. pressing Ctrl and hovering over it does nothing. 
07:44 
pruvisto 
I think "syntax" is the better word here 
07:44 
pruvisto 
"translation" is just the stuff that maps the syntax to actual terms 
07:46 
pruvisto 
hm indeed 
07:46 
pruvisto 
that is unfortunate 
07:46 
pruvisto 
maybe you could ask on the mailing list 
07:46 
pruvisto 
in my naïvete, I think this shouldn't be too hard 
07:46 
pruvisto 
all the information should be there 
08:59 

silver joined #isabelle 
09:38 
larsrh 
I am sorry to inform you that pruvisto is at it again 
09:38 
larsrh 
22nd AFP entry 
10:17 
inte 
soon there'll be enough to fill an Advent calendar 
10:18 
larsrh 
there are currently (including devel) 361 AFP entries 
10:19 
larsrh 
so soon there'll be enough to fill a calender :) 
11:13 

stoopkid joined #isabelle 
11:58 
pruvisto 
I have some more in my pipeline 
11:58 
pruvisto 
at least 3 
11:58 
pruvisto 
Maybe once I have 25 AFP entries I should buy some cake or something to celebrate 
12:30 
larsrh 
no, you should buy a new server 
12:57 
JCaesar 
… 