Time 
Nick 
Message 
01:51 

ilbot3 joined #isabelle 
01:51 

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/ 
04:17 

kini joined #isabelle 
04:30 

kini joined #isabelle 
12:37 
ammbauer 
there's "inj_on (g::'a => 'b) (A::'a set)" and "continuous_on A g" with the arguments switched :P 
12:37 
ammbauer 
this makes isabelle literally unusable :D 
14:29 
inte 
ammbauer: Well that's harmless. Have a look at the definition of refl_on and tell us what you think of that. 
14:30 
inte 
(well, tell me) 
14:33 
ammbauer 
"_on syntax considered harmful" :D 
14:53 
chindy 
what would be better? _wrt ? 
14:53 
chindy 
wasn't there a discussion because of this last weekend? 
14:54 
chindy 
... on the mailing list 
16:07 
inte 
no that was about sorted_by vs. sorted_wrt 
16:07 
inte 
Which is entirely different! 
16:08 
inte 
ammbauer: My complaint ist actually that refl_on A r restricts r to be a subset of A x A. 
16:08 
inte 
Which I found very surprising when I tried to use it. And I ended up not using refl_on at all. 
16:37 
pruvisto 
hm, yes, I see how that may be confusing 
16:37 
pruvisto 
but for things like "order_on"/"linorder_on", that's very convenient 
16:37 
pruvisto 
ammbauer: it gets better 
16:38 
pruvisto 
there's also "holomorphic_on", which is actually infix syntax 
17:01 
inte 
pruvisto: well I was looking for something like order_on, but defined by looking at the restricted relation. 
17:02 
inte 
(this is more of an anecdote than a complaint though) 
19:58 
chindy 
how can i "inspect" the definition of this "overloaded" op+ http://downthetypehole.de/paste/o7kxU2fR 
20:55 
pruvisto 
well, for you, you can do "find_theorems (op + :: _ set => _)" 
20:55 
pruvisto 
it will probably point you to Library/Set_Algebras.thy 
20:56 
pruvisto 
in particular, Set_Algebras.set_plus_def 
20:57 
pruvisto 
(that's actually a somewhat noncanonical name; it should be plus_set_def) 
20:57 
pruvisto 
(cf. plus_real_def, plus_int_def, etc.) 
20:57 
pruvisto 
*well, for one 