<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><blockquote type="cite"><div><font class="Apple-style-span" color="#000000"><br></font></div><div><font class="Apple-style-span" color="#000000"><br></font>Anyway, since eq_reflection actually *is* an axiom, and (=) actually<br>*does* mean the same thing as (==), then I really don't see any reason<br>why we need to have both (or separate bool and prop types, for that<br>matter). I don't know of any other HOL provers that do.<br><br>Even if we got rid of the bool/prop and (=)/(==) distinctions, we<br>still have the "meta-meta-logic" as a natural deduction framework: The<br>"hyps" component of theorems encodes the "is derivable from" relation,<br>and free variables in theorems encode the "this derivation can be done<br>uniformly for all x" property. I have never understood why Isabelle<br>needs multiple levels of meta-logics.<br><br></div></blockquote><div><br></div><div>I agree, these multiple levels are unfortunate ... But I think it is too late to change this now, as frameworks like Isar and many other packages rely on them.</div><div><br></div><div>In a new theorem prover built from scratch (but of course based on many years of Isabelle experience...) this would be one of the lessons learnt ;-)</div><div><br></div><div>Steven </div><div><br></div><div>PS: Now that the Google App Engine is here (with support for Java (that means, also Scala -> Makarius)), wouldn't it be great to make this new theorem prover a native of the cloud?</div><div><br></div><div><br></div><br><blockquote type="cite"><div>- Brian<br>_______________________________________________<br>Isabelle-dev mailing list<br><a href="mailto:Isabelle-dev@mailbroy.informatik.tu-muenchen.de">Isabelle-dev@mailbroy.informatik.tu-muenchen.de</a><br>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br></div></blockquote></div><br></body></html>