Mizar - Isar 比較

• Isarのbyはボディがない証明（proof eqd）の略記。byの直後は証明メソッド。
• Mizarは推論規則の適用とスキーマの適用をby, fromで区別するが、Isarは高階論理なのでbyだけ。
• Isarの前置fromはMizarのfromとは別。Mizarのby相当らしいが要チェック。
• Isarの前置withは前置fromと似ている。要チェック。
• Isarの前置withはMizarのthen ... by相当らしいが。
• Isarのper casesブロックがなく、proof qedで代用。どうしているのか？
• Mizarのsupposeを要チェック。Isarのnext assumeと似ているらしい。Isarのnextも要チェック。
• Mizarのthenがどのタイミングで使うかが分からない。
• Isarのusingを要チェック。