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

All times shown according to UTC.

Time Nick Message
01:37 hazyPurple 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/
04:23 numee joined #isabelle
08:08 hazyPurple joined #isabelle
08:14 chindy pruvisto: interestingly, my textbook says unbounded above means: x : B \and y >= x --> y : B
10:03 pruvisto chindy: in what context?
10:04 chindy pruvisto: consumption sets (economics)
10:05 pruvisto that's a very non-standard notion of "bounded" then
10:06 pruvisto I'd wager if you ask any mathematician for the definition of "bounded from above", she would come up with something very similar to what I said
10:06 pruvisto perhaps the word is used differently in this field
12:10 mal`` joined #isabelle
12:22 chuchuco1ny joined #isabelle
14:24 hazyPurple joined #isabelle
14:47 hazyPurple joined #isabelle
16:37 hazyPurple joined #isabelle
16:55 int-e hmm, is there something like  ultimately note this?  (I have a local proof block, { fix x assume foo  have bar ...  moreover have baz ...  utltimately have bar baz . }  and would like to avoid repeating bar and baz...
17:00 hazyPurple joined #isabelle
17:03 int-e ah: moreover note calculation
17:03 int-e (I may have asked a similar question before. This is a bit obscure.)
17:27 hazyPurple joined #isabelle
18:29 hazyPurple joined #isabelle
19:59 hazyPurple joined #isabelle