Time 
Nick 
Message 
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/ 
09:54 

JCaesar joined #isabelle 
09:58 

cebewee__ joined #isabelle 
14:51 

tangentstorm joined #isabelle 
14:51 

tangentstorm left #isabelle 
16:30 
JCaesar 
Hmm. What effect has ; in apply? I assume that apply(simp; fail) has the effect of either simplifying the goal away or erroring, but I'd like to know more… 
16:39 
inte 
apply (foo; bar) applies foo, and then applies bar to all the subgoals created by foo. 
16:51 
ThreeOfEight 
JCaesar: apply (simp; fail) essentially means "try to solve the goal using simp. If that fails, fail." 
16:51 
ThreeOfEight 
i.e. it's like an "allornothing" version of simp 
16:52 
JCaesar 
which comes in quite handy at times. :) 
16:52 
JCaesar 
inte: ty. 
16:52 
ThreeOfEight 
; is like the "THEN_ALL_NEW" tactical in ML 
16:52 
ThreeOfEight 
there was some discussion whether we want to introduce "solve" as an Isar tactical defined as "solve m = m; fail" 
16:53 
ThreeOfEight 
which can easily be done with Eisbach these days 
16:54 
JCaesar 
Heh, I've always wanted a solve… 
18:24 
JCaesar 
Another thing: How do I get the basic record if I have an extensions record? 
21:19 

larsrh joined #isabelle 