2

イザベル理論 (HOL セッションなど) の HTML ドキュメントを生成したいのですが、証明は含めません。

つまり、 http://isabelle.in.tum.de/library/HOL/Nat.htmlのようなページを作成したい のですが、たとえば、

lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
  apply (rule_tac x = m in spec)
  apply (induct n)
  prefer 2
  apply (rule allI)
  apply (induct_tac x, iprover+)
  done

私だけが見たい

lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"

その理由は、利用可能な定理を調べるために HTML ページを使用しているからですが、その場合、証明は気を散らすだけです。(PDF を生成するときにプルーフを省略できることは知っていますが、特に HTML ドキュメントに興味があります。)

4

2 に答える 2

0

私は最近出力に出くわしcoqdoc、その観点からその質問を理解することができますが、Coq HTML ページにも年齢が表示されるようになりました。

Isabelle では、かつては HTML 表示が非常に重要でしたが、その後、オンラインfind_theoremsまたはオフラインの PDF ドキュメントなどの他のツールがより強力で便利になりました。現在では、Isabelle HTML 出力が最初に登場したときの HTML ブラウザーに近い表示品質を備えた Isabelle/jEdit もあります。実装されました。

現代のIsabelle2013であなたが求めているものを手に入れる簡単な方法はわかりませんが、不可能ではありません。ほとんどの場合、古いものを新しいコンセプトに合わせて改修する必要があります. 静的 Web ページでの HTML ブラウジングは、最近では少し古くなっているため、これまで最優先事項にはなっていませんでした。

いずれにせよ、Isabelle/Scala (Isabelle の公式システム プログラミング インターフェイス) は、たとえば Isabelle/jEdit でオンラインで表示される PIDE ドキュメント マークアップから XML ツリーを取得するためのパブリック API 操作を既に提供しています。そこから、そのビジネスを理解している人にとっては、HTML + CSS まではそれほど遠くありません。ただし、Isabelle/jEdit でいくつかのプレゼンテーションを作成し、多数の Web ブラウザーとその癖をバイパスする方が、より迅速で便利な場合があります。

于 2013-10-09T20:32:54.230 に答える