Email Gateway (Aug 22 2022 at 09:31): Email Gateway (Aug 22 2022 at 09:31):From: "C. Diekmann" <diekmann@in.tum.de>
Dear Makarius,
a small remark where a different output of "print_cases" would have
greatly helped me.
I'm using Isabelle2015-RC2 and I'm trying an Isar-style proof by induction.
proof(induction foo bar baz arbitrary: boo baz rule: somthing.induct)
print_cases
case 1 thus ?case by simp
next
...
so far, everything works fine.
print_cases tells me I also have case "2_1", "2_2", ...
When I try to continue with
case 2_1
I get the error "Outer syntax error⌂: command expected, but symbolic
identifier _⌂ was found".
When I try to continue with
case (2_1)
I get "Undefined case: "2"⌂"
The solution is
case "2_1"
Can print_cases print identifiers which require quoting also in quotes?
Cheers,
Cornelius
Last updated: Apr 25 2024 at 20:15 UTC