Session Modal_Logics_for_NTS

Theories

• HOL-Cardinals.Fun_More
• HOL-Cardinals.Order_Relation_More
• HOL-Cardinals.Wellfounded_More
• HOL-Cardinals.Wellorder_Relation
• HOL-Cardinals.Wellorder_Embedding
• HOL-Cardinals.Order_Union
• HOL-Cardinals.Wellorder_Constructions
• HOL-Cardinals.Ordinal_Arithmetic
• HOL-Cardinals.Cardinal_Order_Relation
• HOL-Cardinals.Cardinal_Arithmetic
• HOL-Cardinals.Wellorder_Extension
• HOL-Cardinals.Cardinals
• HOL-Cardinals.Bounded_Set
• Nominal_Bounded_Set
• Nominal_Wellfounded
• Residual
• Transition_System
• Formula
• Validity
• Logical_Equivalence
• Bisimilarity_Implies_Equivalence
• Equivalence_Implies_Bisimilarity
• Disjunction
• Expressive_Completeness
• FS_Set
• FL_Transition_System
• FL_Formula
• FL_Validity
• FL_Logical_Equivalence
• FL_Bisimilarity_Implies_Equivalence
• FL_Equivalence_Implies_Bisimilarity
• L_Transform
• Weak_Transition_System
• Weak_Formula
• Weak_Validity
• Weak_Logical_Equivalence
• Weak_Bisimilarity_Implies_Equivalence
• Weak_Equivalence_Implies_Bisimilarity
• Weak_Expressive_Completeness
• S_Transform