Camelia, the Perl 6 bug

IRC log for #isabelle, 2013-02-13

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

All times shown according to UTC.

Time Nick Message
01:13 Kaki joined #isabelle
01:14 Kaki joined #isabelle
01:15 kaki joined #isabelle
14:06 felipealmeida joined #isabelle
16:07 kaki joined #isabelle
16:07 kaki hello
16:08 kaki is there a way to use isabelle/isar without excluded-middle?
16:08 kaki that means, as I can avoide using it manually, to make sure isabelle/isar doesn't use it neither automatically
16:09 kaki or to put the question in another way: is there a way to use isabelle/isar for constructive mathematics?
16:12 kaki i know coq can be used that way, but I got already familiar with isabelle/isar and I like some technical features of it
16:17 kaki help is very appreciated
21:00 kaki joined #isabelle
21:45 kaki joined #isabelle
23:37 tsinnema oh nice, over the past few days i had been looking around for various proof assistants, and just now i finally decided to download isabelle -- and lo and behold, a new 2013 is just released
23:37 tsinnema happy timing
23:38 tsinnema a new 2013 version that is

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