# IRC log for #isabelle, 2017-03-16

All times shown according to UTC.

Time Nick Message
02:14 relrod joined #isabelle
02:14 relrod joined #isabelle
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/
03:10 ertes joined #isabelle
04:47 wagle joined #isabelle
07:08 tautologico joined #isabelle
11:43 stoopkid joined #isabelle
12:38 silver joined #isabelle
13:52 int-e why can't I do  finally note foo = this ... sigh.
14:09 pruvisto you do "also note foo = calculation"
14:09 pruvisto but it's really ugly
14:09 pruvisto I wouldn't recommend it ^^
14:09 pruvisto iirc the idea of Isar was to make the proof state explicit frequently
14:10 pruvisto i.e. when you do some long derivation, you explicitly state what you've just proven again
14:10 pruvisto so that a reader will be able to follow it
14:10 pruvisto even without using the IDE
14:10 pruvisto how well that works out in practice is, well, arguable
14:14 int-e thanks, and yes that looks really ugly :-/
14:15 int-e making proof state explicit is fine to some extent but that particular calculation consists of a single application of transitivity... it seems kind of stupid to repeat the two (biggish) terms.
14:17 pruvisto int-e: you probably know this already, but you can introduce abbreviations for sub-terms with pattern matching
14:17 pruvisto e.g. have "biguglyterm = otherbiguglyterm" (is "_ = ?A")
14:18 pruvisto also, if the last thing you've shown is of the form "?f ?x ?y", the term ?y gets implicitly bound to "..." or "…"
14:18 pruvisto so you can write
14:19 pruvisto have "a = b" sorry also have "… = c" sorry also  etc.
14:20 larsrh have "biglyterm = otherbiglyterm"
14:21 pruvisto larsrh: we have the best theorems, I tell you
18:11 ertesx joined #isabelle