FMFI-UK-1-AIN-412 / proof-assistant

Proof assistant
MIT License
0 stars 1 forks source link

Modular theories #4

Open crnkjck opened 6 years ago

crnkjck commented 6 years ago

We want to import (a mutually acyclically depended set of) theories into the currently developed theory so that their axioms and theorems can be used in its proofs. The theories must be browsable, and perhaps even editable.