Commit f81cbfe1 authored by Florian Rabe's avatar Florian Rabe

no message

parent a0b085f9
namespace latin:/❚
import proving scala://latin2/proving❚
theory PropositionsITP =
proof # block proof 1;…❙
rule proving?CheckProof❙
hence # %n L1T by 2❙
suffices # %n 1❙
use # use 1,… ❙
use # use 1❙
rule proving?UseStep❙
theory PLITP =
include ?PropositionsITP❙
assume # %n L1T❙
rule proving?AssumeStep❙
cases # %n 1,…❙
theory SFOLITP =
include ?PLITP❙
fix # %n L1T❙
rule proving?FixStep❙
theory Test : ?SFOLITP =
include ?FOLEQND❙
include ?SFOLEQND❙
test : {A: term ⟶ prop} ⊦ ∀ [x] A x ⇒ A x❘
= [A] proof fix x; assume a; use a❙
test : {T,A: tm T⟶ prop} ⊦ ∀ [x] A x ⇒ A x❘
= [T,A] proof fix x; assume a; use a❙
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment