Dear all,
Jeremy (and I) are encountering some (to us) strange problems with the class-package (it might also be the locale-part, so your expertise is highly welcome here). I am using Isabelle version 20 minutes ago. Attached is a small theory illustrating the problem. Originally, line 32 looked like: embed_nat_even: "!!x. even (embed_nat x) = even x" and but now Isabelle complains about types (apparently inside even_odd we are not allowed to use even with a different type, even if we have already provided an instance). Anyway, when we introduce a silly definition or abbreviation even_nat which is even over nat, we get the following strange error that some tactic in class-package failed. Any idea what this is? In the best case of course someone could tell how to fix it, so we can at least process the theory... Here is the error: *** Tactic failed. *** The error(s) above occurred for the goal statement: *** (!!x::nat. image_nat (embed_nat_class.embed_nat x)) *** ==> (!!x::'a::type. *** image_nat x ==> embed_nat_class.embed_nat (return_nat x) = x) *** ==> (!!(x::nat) y::nat. *** (embed_nat_class.embed_nat x = embed_nat_class.embed_nat y) = *** (x = y)) *** ==> (!!(x::nat) y::nat. *** (embed_nat_class.embed_nat x *** < embed_nat_class.embed_nat y) = *** (x < y)) *** ==> (!!(x::nat) y::nat. *** (embed_nat_class.embed_nat x *** <= embed_nat_class.embed_nat y) = *** (x <= y)) *** ==> (!!(x::nat) y::nat. *** (embed_nat_class.embed_nat x dvd *** embed_nat_class.embed_nat y) = *** (x dvd y)) *** ==> (!!x::nat. *** even (embed_nat_class.embed_nat x) = even_nat x) *** ==> (0::'a::type) = embed_nat_class.embed_nat 0 *** ==> (1::'a::type) = embed_nat_class.embed_nat 1 *** ==> (2::'a::type) = *** embed_nat_class.embed_nat 2 *** ==> (3::'a::type) = *** embed_nat_class.embed_nat 3 *** ==> (!!(x::nat) y::nat. *** embed_nat_class.embed_nat x + embed_nat_class.embed_nat y = *** embed_nat_class.embed_nat (x + y)) *** ==> (!!(x::nat) y::nat. *** y <= x *** ==> embed_nat_class.embed_nat x - *** embed_nat_class.embed_nat y = *** embed_nat_class.embed_nat (x - y)) *** ==> (!!(x::nat) y::nat. *** embed_nat_class.embed_nat x * *** embed_nat_class.embed_nat y = *** embed_nat_class.embed_nat (x * y)) *** ==> (!!(x::nat) n::nat. *** embed_nat_class.embed_nat x ^ n = *** embed_nat_class.embed_nat (x ^ n)) *** ==> (!!(x::nat) y::nat. *** embed_nat_class.embed_nat x div *** embed_nat_class.embed_nat y = *** embed_nat_class.embed_nat (x div y)) *** ==> (!!(x::nat) y::nat. *** embed_nat_class.embed_nat x mod *** embed_nat_class.embed_nat y = *** embed_nat_class.embed_nat (x mod y)) *** ==> ??.Strange.embed_nat op * op div op mod op - *** (1::'a::type) op <= op < op + (0::'a::type) *** number_of even op ^ embed_nat_class.embed_nat *** return_nat image_nat *** At command "class". Best wishes, Amine. -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: Strange.thy URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090123/11939013/attachment.ksh>
