Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2014-12-23

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

All times shown according to UTC.

Time Nick Message
00:01 tangentstorm joined #isabelle
00:53 tangentstorm is it possible to use isar to write proofs about an arbitrary programming language?
00:53 tangentstorm using the syntax of that language i mean
01:30 tangentstorm aha. http://www.concrete-semantics.org/ seems like exactly what i was looking for.
02:48 tangentstorm hrm. src/ZF/ex/NatSum.thy seems to be broken on a fresh install.
02:48 tangentstorm consts sum :: "[i=>i, i] => i"  says Undefined type name: "i"
02:49 tangentstorm do I have to do something to make it use zf instead of hol?
06:10 tangentstorm okay, i did figure that one out, and documented it here: http://stackoverflow.com/questions/27613657/how-to-make-isabelle-use-zf
06:11 tangentstorm but i'm stuck on a new problem. i posted it on stackoverflow, too, in case anyone here wakes up and decides to have mercy on me. :)
06:11 tangentstorm http://stackoverflow.com/questions/27614983/expressing-a-simple-declarative-proof-about-exponents-in-isar
08:49 tangentstorm hrm. any way to make "test" another alias for "lemma"/"theorem" ?
12:25 lrabiet joined #isabelle
12:27 wagle joined #isabelle

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