no message

source/argumentation.mmt

+namespace http://cds.omdoc.org/examples❚
+
+theory TopologicalArgumentationTheory : http://cds.omdoc.org/urtheories?LF =
+  include ?PL❙
+  
+  K : prop ⟶ prop❙
+  B : prop ⟶ prop❙
+  box: prop  ⟶ prop ❘ # □ 1❙
+
+  world : type❙
+  
+  argument: type❙
+  attacks : argument ⟶ argument ⟶ type ❘# 1 ← 2❙
+  
+  in : world ⟶ argument ⟶ type ❘# 1 ‍∈ 2❙
+  holds : world ⟶ prop ⟶ type ❘ # 1 ⊧ 2❙
+  Fix : argument ⟶ type❙
+  
+  holds_conj : {w,F,G} w ⊧ F ⟶ w ⊧ G ⟶ w ⊧ F ∧ G❙
+  holds_disj1 : {w,F,G} w ⊧ F ⟶ w ⊧ F ∨ G❙
+  holds_disj2 : {w,F,G} w ⊧ G ⟶ w ⊧ F ∨ G❙
+  
+  holds_K : {w,F} ({v} v ⊧ F) ⟶ w ⊧ K F❙
+  holds_box : {w,F,T} w ‍∈ T ⟶ ({v} v ‍∈ T ⟶ v ⊧ F) ⟶ w ⊧ □ F❙
+  holds_B : {w,F,T} w ‍∈ T ⟶ Fix T ⟶ ({v} v ‍∈ T ⟶ v ⊧ F) ⟶ w ⊧ B F❙
+❚
\ No newline at end of file

source/logic/pl.mmt

@@ -37,7 +37,7 @@ theory PL : http://cds.omdoc.org/urtheories?LF =
 ❚
 
 /T   Now we describe the proof theory.❚        
-        
+
 theory PLNatDed : http://cds.omdoc.org/urtheories?LF =
   include ?PL ❙