私はちょうどIsabelle/HOLから始まり、単純なHOLステートメント "P（t）⟶（∃x。P（x））"を自然控除ルールで証明しようとしています。位置で theory simple imports Main
begin
lemma T: shows "P(t) ⟶ (∃x . P(x))"
proof
(* x *)
qed
end
コメントにXをマークし、現在の目
ノートなぜ機能（クラス）の以下の定義 definition nondecreasing_on :: "real set => (real => real) => bool"
where "nondecreasing_on S f <-> (ALL x:S. ALL y:S. x<=y --> f x <= f y)"
リターンInner syntax error⌂ Failed to par
Isabelle（バージョン2016-1）で遊んでいるときに、次のような奇妙な状況が発生しました。さまざまな変数または関数名として文字oを使用できません（ほとんどの/すべて？）コンテキスト。 （？すべての）次の例はすべて、ほとんどの作業にもかかわらず、失敗する英語のアルファベットの他の文字： value o (* quoted version doesn't work either *)
de
私はIsabelleを初めて使用しています。私は基本的な再帰関数を定義しようとしています。私は追加してみましたが、私は乗算に問題があります。 datatype nati = Zero | Suc nati
primrec add :: "nati ⇒ nati ⇒ nati" where
"add Zero n = n" |
"add (Suc m) n = Suc(add m n)"