# IRC log for #isabelle, 2016-01-06

All times shown according to UTC.

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 int-e 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 "all-or-nothing" version of simp
16:52 JCaesar which comes in quite handy at times. :)
16:52 JCaesar int-e: 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