sfja/sfja — Issue #15: Prop_J.html で文書が切れてます。
Author: buynnnmmm1
Created: 2012-02-10 09:09:07+00:00
State: open

この訳のお陰で大変楽してCoqの勉強ができます。本当にありがとうございます。

Prop_J.v では文書切れてないのですが、htmlの方で文書が途中で切れてしまってます。

場所は「偶数について再び」の一つ前の文書です。

.... 、それによって[P]が[S n'

でhtmlは文書が終ってしまっており、Prop_J.vで該当の部分は

、それによって[P]が[S n']について成り立つことを示すことができます。
*)

となっていて、文書切れていません。

よろしくお願い致します。