Camelia, the Perl 6 bug

IRC log for #isabelle, 2012-05-20

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

All times shown according to UTC.

Time Nick Message
09:14 Kaki joined #isabelle
09:14 Kaki Hello!
09:14 Kaki I got this message "The prover found a type-unsound proof involving ""13"", ""22"", ""9"", "a", "c", and "lema3_7" even though a supposedly type-sound encoding was used (or, less likely, your axioms are inconsistent). Please report this to the Isabelle developers."
09:15 Kaki from my Isabelle/Hol system.
09:15 Kaki Do you have an idea where to report that?
10:33 Kaki I found the responsable person through looking in a user manual written for the Sledgehammer tool

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