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/ 
05:13 

mal``` joined #isabelle 
05:43 

lispy joined #isabelle 
10:29 

larsrh joined #isabelle 
10:30 

silver joined #isabelle 
12:27 

ilbot3 joined #isabelle 
12:27 

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/ 
12:47 

ilbot3 joined #isabelle 
12: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/ 
13:09 

ilbot3 joined #isabelle 
13:09 

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/ 
13:43 

ilbot3 joined #isabelle 
13:43 

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/ 
14:19 

ilbot3 joined #isabelle 
14:19 

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/ 
14:52 

ilbot3 joined #isabelle 
14:52 

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/ 
15:24 

ilbot3 joined #isabelle 
15:24 

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/ 
15:46 

ilbot3 joined #isabelle 
15:46 

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/ 
15:55 

ilbot3 joined #isabelle 
15:55 

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/ 
16:15 

ilbot3 joined #isabelle 
16:15 

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/ 
16:20 
ammbauer 
what rule do I have to add to auto, if I have something like "case xs of [] => P  x#xs' => Q" in my assumptions and I want it to case split automatically? 
16:26 
larsrh 
split: list.splits 
16:27 
ammbauer 
huh, okay. now it's working ;shrug 
22:03 

qwertyyyy joined #isabelle 
23:42 
qwertyyyy 
what does it mean when I use quickcheck on a lemma and for P in a expression like P x it finds a counterexample "{}" or something similar 
23:42 
qwertyyyy 
for example : 
23:42 
qwertyyyy 
"(P z) ⟹ ( P y )" 
23:43 
qwertyyyy 
quickcheck finds : P = {a_1} ; z = a_1 ; y = a_2 
23:44 
qwertyyyy 
I understand why it is wrong ... I just don't understand what quickcheck wants me to tell by "P = {a_1}" 