# IRC log for #isabelle, 2017-08-18

All times shown according to UTC.

Time Nick Message
01:24 mal`` joined #isabelle
01:42 keep_learning joined #isabelle
01:51 ilbot3 joined #isabelle
01:51 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:14 chindy is there a power function with ints instead of nats ? or would one have to write 1/10^n instead of 10^-n
11:57 int-e . o O ( is this sane?  apply (subst foo; (simp; fail)?), where the idea is that simp will squash the preconditions... )
12:04 pruvisto sure
12:04 pruvisto not sure about the ? though
12:14 dave24 joined #isabelle
12:18 int-e pruvisto: well, one subgoal remains.
12:18 pruvisto ah I see
12:18 int-e (I'd love to specify that fact but I don't know how)
12:18 pruvisto but shouldn't it then be "(simp; fail)+?"
12:19 int-e note the ; after the subst
12:19 pruvisto oh right
12:19 pruvisto I'm too old for this
12:20 int-e old dog, eh
12:20 int-e this chain of substs is getting too long, I'm 6 levels deep already
12:21 pruvisto Well I'm 26
12:21 pruvisto but I've been using Isabelle for 6 years, long before ";" was around ^^
12:22 chindy what does ; do ?
12:23 dave24 joined #isabelle
12:29 chindy pruvisto: also i was wondering if you could point me to a "text book" -style isabelle proof SUM 1/2^n -> inf approaches 2
12:30 chindy aka some text book epsilon delta proofs in isablle
12:30 pruvisto I don't think anybody does epsilon-delta proofs in Isabelle
12:30 pruvisto except maybe Jeremy Avigad like ten years ago
12:30 pruvisto there's no reason to do that
12:30 pruvisto reasoning with filters is much cleaner and easier
12:32 chindy pruvisto:  ohh i see... so can you point me to some "good" well structured proofs of this kind?
12:32 pruvisto hmm, I don't know
12:32 pruvisto not off the top of my head
12:32 pruvisto I can recommend reading the tutorial on filters
12:33 pruvisto it takes a while to get your head around this, but they unify a lot of these topological notions of "neighbourhood" and "limits" very nicely
12:35 chindy by hölzl/Huffman...?
12:36 pruvisto yes
15:12 juanbono joined #isabelle
19:34 dmiles joined #isabelle
21:12 larsrh as promised: https://dl.bintray.com/larsrh/libisabelle/nightly/isabellectl
21:16 larsrh (2017-RC0 support)