# IRC log for #isabelle, 2017-02-21

All times shown according to UTC.

Time Nick Message
02:25 throwaway-irc_ joined #isabelle
02:26 throwaway-irc_ is there a difference between 'assumes "A" shows "B"' and "A ==> B"? if so, are they interconvertible? or at least can I convert proofs of "A ==> B" into those of 'assumes "A" shows "B"'?
06:49 pruvisto ugh, this is tricky
06:49 pruvisto this is some really technical aspect of Isar, /and/ it changed a year ago or so and now I don't know at all anymore
06:50 pruvisto In principle, you should not write something like "have "A ==> B"" at all
06:50 pruvisto you should rater write "assume A have B" (in a local proof block with { … }, if necessary)
06:50 pruvisto or the new "have A if B" syntax
06:51 pruvisto This might be easier to explain if you give me a concrete example
12:07 silver joined #isabelle
15:10 kini joined #isabelle
17:05 silver_ joined #isabelle
23:02 JCaesar pruvisto: Isn't it that with have "A ==> B" you'll have to do a proof -  assume A, with have B if A you'll just get the assumptions named that (and can name them)?
23:03 JCaesar (Also, as a rule of thumb, I'd say you should avoid {}-subproofs (because note foo = this), use have B if A if you continue with an isar-proof, and have "A ==> B" if it's just a single method / apply style. But that's just my personal experience.)
23:04 JCaesar Why would you say one shouldn't write have "A ==> B"? (I write lemma "A ==> B" all the time. Is that also bad?)