Time 
Nick 
Message 
02:48 

ilbot3 joined #isabelle 
02: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/ 
04:39 
AtnNn 
Is there a shorter way of writing `show "EX x . P(x)" proof show "P(w)" by rule qed'? 
06:53 
ThreeOfEight 
AtnNn: "by (rule exI[of _ w])" 
06:54 
ThreeOfEight 
or "have "P w" by (whatever)" and then "thus "∃x. P x" .." 
06:54 
ThreeOfEight 
where ".." is an abbreviation for "by rule" 
08:49 
JCaesar 
And where by rule will pick the default rule, which is exI in that case… (right? How does that work, btw?) 
10:28 

silver joined #isabelle 
11:05 
ThreeOfEight 
JCaesar: I think it just nondeterministically picks a matching rule that was declared intro, intro!, or intro? 
11:08 
ThreeOfEight 
also elim, apparently 
11:10 
ThreeOfEight 
there's a structure called "claset" where rules like this are stored 
11:10 
ThreeOfEight 
see ~~/src/Provers/classical.ML 
11:36 

silver joined #isabelle 
14:44 

ammbauer joined #isabelle 
15:05 

ammbauer joined #isabelle 
16:42 
AtnNn 
Thanks 