[isabelle] Eisbach: HOL vs. Pure



Dear Makarius and Dan,

what is the reason for Eisbach residing in HOL instead of Pure? As far
as I can tell, the only dependency on HOL is for the "match" method,
which treats "Trueprop" specially (makes sense to me), but appears to
also deal with numerals (I don't understand the corresponding sources).

Anyway, making an exact copy of "Eisbach.thy", removing the line

  ML_file "match_method.ML"

... and changing the import from "Main" to "Pure", it still works. I've
made a tiny experiment with some "simp" and "rule" invocations and the
method I defined behaves exactly as expected.

Cheers
Lars




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