Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-08-01

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
00:05 keep_learning joined #isabelle
00:13 aindilis` joined #isabelle
00:22 https_GK1wmSU joined #isabelle
00:22 https_GK1wmSU left #isabelle
00:22 https_GK1wmSU joined #isabelle
00:25 https_GK1wmSU left #isabelle
00:26 stoopkid_ joined #isabelle
00:55 aindilis 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/
02:47 https_GK1wmSU joined #isabelle
02:47 https_GK1wmSU left #isabelle
10:53 chindy is there some shematic variable like ?thesis but for the current subgoal ?
10:53 chindy like ?goal or something
11:06 JCaesar ?case is often set.
11:06 JCaesar iirc, there's some print_* or show_* that will display that.
11:06 JCaesar (There is ?goal1, but you shouldn't.)
11:08 JCaesar If nothing is set, you can do a proof ((…), goal_cases), where … is whatever proof method you were using before. then, you can use case 1 thus ?case.
11:08 JCaesar Isabelle/jEdit should even suggest that case 1 thus ?case thing if it is available.
16:07 int-e goal_cases is my most favorite recent discovery.
17:19 juanbono joined #isabelle
22:17 JCaesar s/discovery/addition to Isabelle/ ;)

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary