# IRC log for #isabelle, 2017-08-22

All times shown according to UTC.

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 int-e ammbauer: Well that's harmless. Have a look at the definition of refl_on and tell us what you think of that.
14:30 int-e (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 int-e no that was about sorted_by vs. sorted_wrt
16:07 int-e Which is entirely different!
16:08 int-e ammbauer: My complaint ist actually that refl_on A r restricts r to be a subset of A x A.
16:08 int-e 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 int-e pruvisto: well I was looking for something like order_on, but defined by looking at the restricted relation.
17:02 int-e (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 non-canonical name; it should be plus_set_def)
20:57 pruvisto (cf. plus_real_def, plus_int_def, etc.)
20:57 pruvisto *well, for one