[isabelle] print_statement and sorts



Hi all,

print_statement is a nice feature, as it prints a theorem in long-goal
format, ready to be copied into the edit-buffer, e.g. to slightly modify
it.

However, if sorts are involved, the printed statement is, in many cases,
just not valid, as sort constraints are omitted:

print_statement order_refl

theorem order_refl:
  fixes x :: "'a" 
  shows "x ≤ x"

*** Type unification failed: Variable 'a::type not of sort ord


Using show_sorts is also not what I really want, as the sort-annotations
pop up in the term, too:

theorem order_refl:
  fixes x :: "'a∷preorder" 
  shows "(x∷'a∷preorder) ≤ x"

The best way might be to make print_statement only print non-default
sorts in the fixes-part.


--
  Peter





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