# IRC log for #isabelle, 2017-01-26

All times shown according to UTC.

Time Nick Message
00:16 ski joined #isabelle
02:47 ilbot3 joined #isabelle
02:47 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/
11:27 silver joined #isabelle
11:38 silver_ joined #isabelle
13:04 larsrh yay, named sublocale interpretation chains: rules_as_nrules.crules_as_irules'.irules'_as_irules.compile_correct_rt
13:05 int-e readable like a book
13:15 pruvisto larsrh: find ./ -name "*.thy" -exec grep "\blocale\b" {} \; | wc -l
13:55 larsrh lemma assumes "set xs = insert x S" "x ∉ S" obtains xs' where "xs = x # xs'" "set xs' = S"
13:55 larsrh I'm having an unreasonable amount of trouble proving this
13:56 larsrh it's basically an elim rule for 'set'
14:36 pruvisto larsrh: I don't think this is true
14:37 pruvisto larsrh: http://downthetypehole.de/paste/Lia9jhdb
14:38 pruvisto That might explain the trouble you're having in proving it. :P
14:39 pruvisto The basic problem is that there's absolutely no reason why the "x" should have to be the first element of the list
15:53 stoopkid joined #isabelle
17:02 logicmoo joined #isabelle
20:20 larsrh pruvisto: you're such a spoilsport
20:53 pruvisto larsrh: you mean a kaziŝuk? :P
20:53 pruvisto *kazišuk
22:20 silver joined #isabelle