[isabelle] [2015-RC2] print_cases and underscore case names



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.