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 
inte 
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 