[isabelle] read/print consistency?
Is there supposed to be any sort of guarantee of consistency between a
term A and the term B that results from printing A and then reading
the result, when the "show types" option is off? I have found a case
where the types in B are more general, in a way that caused problems
trying to do a lemma. I can give more details if desired.
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)
This archive was generated by a fusion of
Pipermail (Mailman edition) and