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 
inte 
. 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 
inte 
pruvisto: well, one subgoal remains. 
12:18 
pruvisto 
ah I see 
12:18 
inte 
(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 
inte 
note the ; after the subst 
12:19 
pruvisto 
oh right 
12:19 
pruvisto 
I'm too old for this 
12:20 
inte 
old dog, eh 
12:20 
inte 
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 epsilondelta 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 
(2017RC0 support) 