Commit 2fbf906e authored by Florian Rabe's avatar Florian Rabe

no message

parent b7b48874
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/pl.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#0.0.0:4091.136.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://cds.omdoc.org/examples"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#206.8.0:268.8.62"/></metadata>We use LF as the meta-theory for all theories in this file.</opaque><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#315.11.0:370.12.48"/></metadata>We start with the syntax of propositional logic.</opaque><mref name="[http://cds.omdoc.org/examples?PL]" target="http://cds.omdoc.org/examples?PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#373.14.0:381.14.8"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1425.46.0:1463.46.38"/></metadata>Now we describe the proof theory.</opaque><mref name="[http://cds.omdoc.org/examples?PLNatDed]" target="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1474.48.0:1488.48.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?DeclarativeProofs]" target="http://cds.omdoc.org/examples?DeclarativeProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#2996.92.0:3019.92.23"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Declarative_PL]" target="http://cds.omdoc.org/examples?Declarative_PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#3169.101.0:3189.101.20"/></metadata></mref><instruction text="import rules scala://lf.mmt.kwarc.info"/><mref name="[http://cds.omdoc.org/examples?ProofIrrelevance]" target="http://cds.omdoc.org/examples?ProofIrrelevance"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#3958.132.0:3980.132.22"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/logic/pl.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#0.0.0:4103.136.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://cds.omdoc.org/examples"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#206.8.0:268.8.62"/></metadata>We use LF as the meta-theory for all theories in this file.</opaque><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#315.11.0:370.12.48"/></metadata>We start with the syntax of propositional logic.</opaque><mref name="[http://cds.omdoc.org/examples?PL]" target="http://cds.omdoc.org/examples?PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#373.14.0:381.14.8"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1437.46.0:1475.46.38"/></metadata>Now we describe the proof theory.</opaque><mref name="[http://cds.omdoc.org/examples?PLNatDed]" target="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1486.48.0:1500.48.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?DeclarativeProofs]" target="http://cds.omdoc.org/examples?DeclarativeProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#3008.92.0:3031.92.23"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Declarative_PL]" target="http://cds.omdoc.org/examples?Declarative_PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#3181.101.0:3201.101.20"/></metadata></mref><instruction text="import rules scala://lf.mmt.kwarc.info"/><mref name="[http://cds.omdoc.org/examples?ProofIrrelevance]" target="http://cds.omdoc.org/examples?ProofIrrelevance"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#3970.132.0:3992.132.22"/></metadata></mref></omdoc>
\ No newline at end of file
......@@ -3,6 +3,7 @@ dataconstructor http://cds.omdoc.org/examples/epa?DependentFunctionTypes?[http:/
theory http://cds.omdoc.org/examples/epa?DependentFunctionTypes
HasMeta http://cds.omdoc.org/examples/epa?DependentFunctionTypes http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?DependentFunctionTypes http://cds.omdoc.org/examples/epa?TypedTerms
Includes http://cds.omdoc.org/examples/epa?DependentFunctionTypes http://cds.omdoc.org/examples/epa?Types
Declares http://cds.omdoc.org/examples/epa?DependentFunctionTypes http://cds.omdoc.org/examples/epa?DependentFunctionTypes?depfun
constant http://cds.omdoc.org/examples/epa?DependentFunctionTypes?depfun
DependsOn http://cds.omdoc.org/examples/epa?DependentFunctionTypes?depfun?type http://cds.omdoc.org/examples/epa?Types?tp?type
......
......@@ -4,7 +4,14 @@ dataconstructor http://cds.omdoc.org/examples/epa?DependentFunctions?depbeta
theory http://cds.omdoc.org/examples/epa?DependentFunctions
HasMeta http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?DependentFunctionTypes
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?TypedTerms
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?SimpleFunctionTypes
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?TypedEquality
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?TypedLogic
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?Proofs
Declares http://cds.omdoc.org/examples/epa?DependentFunctions http://cds.omdoc.org/examples/epa?DependentFunctions?deplambda
constant http://cds.omdoc.org/examples/epa?DependentFunctions?deplambda
DependsOn http://cds.omdoc.org/examples/epa?DependentFunctions?deplambda?type http://cds.omdoc.org/examples/epa?DependentFunctionTypes?depfun?type
......
......@@ -4,6 +4,10 @@ dataconstructor http://cds.omdoc.org/examples/epa?Equality?congP
theory http://cds.omdoc.org/examples/epa?Equality
HasMeta http://cds.omdoc.org/examples/epa?Equality http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?Equality http://cds.omdoc.org/examples/epa?UntypedLogic
Includes http://cds.omdoc.org/examples/epa?Equality http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?Equality http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?Equality http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?Equality http://cds.omdoc.org/examples/epa?Terms
Declares http://cds.omdoc.org/examples/epa?Equality http://cds.omdoc.org/examples/epa?Equality?equal
constant http://cds.omdoc.org/examples/epa?Equality?equal
DependsOn http://cds.omdoc.org/examples/epa?Equality?equal?type http://cds.omdoc.org/examples/epa?Propositions?prop?type
......
......@@ -3,6 +3,7 @@ datatypeconstructor http://cds.omdoc.org/examples/epa?InternalPropositions?[http
theory http://cds.omdoc.org/examples/epa?InternalPropositions
HasMeta http://cds.omdoc.org/examples/epa?InternalPropositions http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?InternalPropositions http://cds.omdoc.org/examples/epa?TypedTerms
Includes http://cds.omdoc.org/examples/epa?InternalPropositions http://cds.omdoc.org/examples/epa?Types
Declares http://cds.omdoc.org/examples/epa?InternalPropositions http://cds.omdoc.org/examples/epa?InternalPropositions?bool
constant http://cds.omdoc.org/examples/epa?InternalPropositions?bool
DependsOn http://cds.omdoc.org/examples/epa?InternalPropositions?bool?type http://cds.omdoc.org/examples/epa?Types?tp?type
......
......@@ -10,6 +10,10 @@ dataconstructor http://cds.omdoc.org/examples/epa?InternalTypes?typesAsPredicate
theory http://cds.omdoc.org/examples/epa?InternalTypes
HasMeta http://cds.omdoc.org/examples/epa?InternalTypes http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?InternalTypes http://cds.omdoc.org/examples/epa?UntypedLogic
Includes http://cds.omdoc.org/examples/epa?InternalTypes http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?InternalTypes http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?InternalTypes http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?InternalTypes http://cds.omdoc.org/examples/epa?Terms
Declares http://cds.omdoc.org/examples/epa?InternalTypes http://cds.omdoc.org/examples/epa?InternalTypes?in
constant http://cds.omdoc.org/examples/epa?InternalTypes?in
DependsOn http://cds.omdoc.org/examples/epa?InternalTypes?in?type http://cds.omdoc.org/examples/epa?Propositions?prop?type
......
......@@ -2,6 +2,14 @@ dataconstructor http://cds.omdoc.org/examples/epa?SimpleFunctionsEta?eta
theory http://cds.omdoc.org/examples/epa?SimpleFunctionsEta
HasMeta http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?SimpleFunctions
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?SimpleFunctionTypes
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?TypedEquality
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?TypedLogic
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?TypedTerms
Declares http://cds.omdoc.org/examples/epa?SimpleFunctionsEta http://cds.omdoc.org/examples/epa?SimpleFunctionsEta?eta
constant http://cds.omdoc.org/examples/epa?SimpleFunctionsEta?eta
DependsOn http://cds.omdoc.org/examples/epa?SimpleFunctionsEta?eta?type http://cds.omdoc.org/examples/epa?Proofs?ded?type
......
......@@ -2,6 +2,14 @@ dataconstructor http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality?
theory http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality
HasMeta http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?SimpleFunctions
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?SimpleFunctionTypes
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?TypedEquality
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?TypedLogic
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?TypedTerms
Declares http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality?exten
constant http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality?exten
DependsOn http://cds.omdoc.org/examples/epa?SimpleFunctionsExtensionality?exten?type http://cds.omdoc.org/examples/epa?Proofs?ded?type
......
......@@ -4,7 +4,13 @@ dataconstructor http://cds.omdoc.org/examples/epa?SimpleFunctions?simpbeta
theory http://cds.omdoc.org/examples/epa?SimpleFunctions
HasMeta http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?SimpleFunctionTypes
Includes http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?TypedEquality
Includes http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?TypedLogic
Includes http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?TypedTerms
Declares http://cds.omdoc.org/examples/epa?SimpleFunctions http://cds.omdoc.org/examples/epa?SimpleFunctions?simplambda
constant http://cds.omdoc.org/examples/epa?SimpleFunctions?simplambda
DependsOn http://cds.omdoc.org/examples/epa?SimpleFunctions?simplambda?type http://cds.omdoc.org/examples/epa?SimpleFunctionTypes?simpfun?type
......
......@@ -2,6 +2,9 @@ dataconstructor http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes?sof
theory http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes
HasMeta http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes http://cds.omdoc.org/examples/epa?SoftTypedTerms
Includes http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes http://cds.omdoc.org/examples/epa?Terms
Includes http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes http://cds.omdoc.org/examples/epa?Propositions
Declares http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes?softfun
constant http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes?softfun
DependsOn http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes?softfun?type http://cds.omdoc.org/examples/epa?Types?tp?type
......
......@@ -2,7 +2,16 @@ dataconstructor http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions?fu
theory http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions
HasMeta http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?SoftTypedTerms
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?Terms
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?SoftTypedFunctions
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?SoftTypedEquality
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?SoftTypedLogic
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?Equality
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?UntypedLogic
Includes http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?SoftDependentFunctionTypes
Declares http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions?fun_typing
constant http://cds.omdoc.org/examples/epa?SoftTypedDependentFunctions?fun_typing
......
theory http://cds.omdoc.org/examples/epa?SoftTypedEquality
HasMeta http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?SoftTypedLogic
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?SoftTypedTerms
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?Terms
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?Equality
Includes http://cds.omdoc.org/examples/epa?SoftTypedEquality http://cds.omdoc.org/examples/epa?UntypedLogic
......@@ -5,6 +5,14 @@ theory http://cds.omdoc.org/examples/epa?SoftTypedFunctions
HasMeta http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?Terms
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?SoftTypedEquality
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?SoftTypedLogic
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?SoftTypedTerms
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?Equality
Includes http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?UntypedLogic
Declares http://cds.omdoc.org/examples/epa?SoftTypedFunctions http://cds.omdoc.org/examples/epa?SoftTypedFunctions?lambda
constant http://cds.omdoc.org/examples/epa?SoftTypedFunctions?lambda
DependsOn http://cds.omdoc.org/examples/epa?SoftTypedFunctions?lambda?type http://cds.omdoc.org/examples/epa?Terms?term?type
......
theory http://cds.omdoc.org/examples/epa?SoftTypedLogic
HasMeta http://cds.omdoc.org/examples/epa?SoftTypedLogic http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SoftTypedLogic http://cds.omdoc.org/examples/epa?SoftTypedTerms
Includes http://cds.omdoc.org/examples/epa?SoftTypedLogic http://cds.omdoc.org/examples/epa?Terms
Includes http://cds.omdoc.org/examples/epa?SoftTypedLogic http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SoftTypedLogic http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?SoftTypedLogic http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?SoftTypedLogic http://cds.omdoc.org/examples/epa?Proofs
......@@ -2,7 +2,16 @@ dataconstructor http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions?fun_t
theory http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions
HasMeta http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?SoftTypedTerms
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?Terms
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?Types
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?SoftTypedFunctions
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?SoftTypedEquality
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?SoftTypedLogic
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?Equality
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?UntypedLogic
Includes http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?SimpleFunctionTypes
Declares http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions?fun_typing
constant http://cds.omdoc.org/examples/epa?SoftTypedSimpleFunctions?fun_typing
......
......@@ -7,6 +7,11 @@ dataconstructor http://cds.omdoc.org/examples/epa?TypedEquality?trans
theory http://cds.omdoc.org/examples/epa?TypedEquality
HasMeta http://cds.omdoc.org/examples/epa?TypedEquality http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?TypedEquality http://cds.omdoc.org/examples/epa?TypedLogic
Includes http://cds.omdoc.org/examples/epa?TypedEquality http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?TypedEquality http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?TypedEquality http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?TypedEquality http://cds.omdoc.org/examples/epa?TypedTerms
Includes http://cds.omdoc.org/examples/epa?TypedEquality http://cds.omdoc.org/examples/epa?Types
Declares http://cds.omdoc.org/examples/epa?TypedEquality http://cds.omdoc.org/examples/epa?TypedEquality?equal
constant http://cds.omdoc.org/examples/epa?TypedEquality?equal
DependsOn http://cds.omdoc.org/examples/epa?TypedEquality?equal?type http://cds.omdoc.org/examples/epa?Types?tp?type
......
theory http://cds.omdoc.org/examples/epa?TypedLogic
HasMeta http://cds.omdoc.org/examples/epa?TypedLogic http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?TypedLogic http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?TypedLogic http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?TypedLogic http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?TypedLogic http://cds.omdoc.org/examples/epa?TypedTerms
Includes http://cds.omdoc.org/examples/epa?TypedLogic http://cds.omdoc.org/examples/epa?Types
theory http://cds.omdoc.org/examples/epa?UntypedLogic
HasMeta http://cds.omdoc.org/examples/epa?UntypedLogic http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/examples/epa?UntypedLogic http://cds.omdoc.org/examples/epa?Logic
Includes http://cds.omdoc.org/examples/epa?UntypedLogic http://cds.omdoc.org/examples/epa?Propositions
Includes http://cds.omdoc.org/examples/epa?UntypedLogic http://cds.omdoc.org/examples/epa?Proofs
Includes http://cds.omdoc.org/examples/epa?UntypedLogic http://cds.omdoc.org/examples/epa?Terms
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