the next generation of the in-browser educational proof assistant
add back nat prooftest
+9
+9
index.html
+9
index.html
···
342
342
</hol-comp>
343
343
<hol-config id="index.html/myconfig">Gentzen</hol-config>
344
344
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat">
345
+
a.
346
+
(Nat a)
347
+
-------
348
+
(Nat (S (S a)))
349
+
350
+
a. asm |- ?
351
+
</hol-proof>
352
+
353
+
<hol-proof id="index.html/prooftest2" deps="index.html/myconfig index.html/baz index.html/nat">
345
354
a. b. f.
346
355
(= a b)
347
356
-------