Skipping 1,295 KB.. Full Log

Presenting theory Myhill-Nerode.Non_Regular_Languages
20:15:17 Presenting Order_Lattice_Props ...
20:15:17 Presenting document Order_Lattice_Props/document
20:15:17 Presenting document Order_Lattice_Props/outline
20:15:17 Presenting theory Order_Lattice_Props.Sup_Lattice
20:15:17 Presenting theory Order_Lattice_Props.Order_Duality
20:15:17 Presenting theory Order_Lattice_Props.Order_Lattice_Props
20:15:17 Presenting theory Order_Lattice_Props.Representations
20:15:17 Presenting theory Order_Lattice_Props.Galois_Connections
20:15:17 Presenting theory Order_Lattice_Props.Fixpoint_Fusion
20:15:17 Presenting theory Order_Lattice_Props.Closure_Operators
20:15:17 Presenting theory Order_Lattice_Props.Order_Lattice_Props_Loc
20:15:17 Presenting theory Order_Lattice_Props.Order_Lattice_Props_Wenzel
20:15:17 Presenting Quantales ...
20:15:17 Presenting document Quantales/document
20:15:17 Presenting document Quantales/outline
20:15:17 Presenting theory Quantales.Dioid_Models_New
20:15:17 Presenting theory Quantales.Quantales
20:15:17 Presenting theory Quantales.Quantale_Star
20:15:17 Presenting theory Quantales.Quantale_Modules
20:15:17 Presenting theory Quantales.Quantale_Models
20:15:17 Presenting theory Quantales.Quantic_Nuclei_Conuclei
20:15:17 Presenting theory Quantales.Quantale_Left_Sided
20:15:18 Presenting Transformer_Semantics ...
20:15:18 Presenting document Transformer_Semantics/document
20:15:18 Presenting document Transformer_Semantics/outline
20:15:18 Presenting theory Transformer_Semantics.Isotone_Transformers
20:15:18 Presenting theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
20:15:18 Presenting theory Transformer_Semantics.Powerset_Monad
20:15:18 Presenting theory Transformer_Semantics.Kleisli_Transformers
20:15:18 Presenting theory Transformer_Semantics.Kleisli_Quantaloid
20:15:18 Presenting theory Transformer_Semantics.Kleisli_Quantale
20:15:18 Presenting Ordered_Resolution_Prover ...
20:15:18 Presenting document Ordered_Resolution_Prover/document
20:15:18 Presenting document Ordered_Resolution_Prover/outline
20:15:18 Presenting theory Ordered_Resolution_Prover.Map2
20:15:18 Presenting theory Ordered_Resolution_Prover.Lazy_List_Liminf
20:15:18 Presenting theory Ordered_Resolution_Prover.Lazy_List_Chain
20:15:18 Presenting theory Ordered_Resolution_Prover.Clausal_Logic
20:15:18 Presenting theory Ordered_Resolution_Prover.Herbrand_Interpretation
20:15:18 Presenting theory Ordered_Resolution_Prover.Abstract_Substitution
20:15:18 Presenting theory Ordered_Resolution_Prover.Inference_System
20:15:18 Presenting theory Ordered_Resolution_Prover.Ground_Resolution_Model
20:15:18 Presenting theory Ordered_Resolution_Prover.Unordered_Ground_Resolution
20:15:18 Presenting theory Ordered_Resolution_Prover.Ordered_Ground_Resolution
20:15:18 Presenting theory Ordered_Resolution_Prover.Proving_Process
20:15:18 Presenting theory Ordered_Resolution_Prover.Standard_Redundancy
20:15:18 Presenting theory Ordered_Resolution_Prover.FO_Ordered_Resolution
20:15:18 Presenting theory Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover
20:15:19 Presenting Chandy_Lamport ...
20:15:19 Presenting document Chandy_Lamport/document
20:15:19 Presenting document Chandy_Lamport/outline
20:15:19 Presenting theory Chandy_Lamport.Distributed_System
20:15:19 Presenting theory Chandy_Lamport.Trace
20:15:19 Presenting theory Chandy_Lamport.Util
20:15:19 Presenting theory Chandy_Lamport.Swap
20:15:19 Presenting theory Chandy_Lamport.Snapshot
20:15:19 Presenting theory Chandy_Lamport.Co_Snapshot
20:15:19 Presenting theory Chandy_Lamport.Example
20:15:21 Presenting Functional_Ordered_Resolution_Prover ...
20:15:21 Presenting document Functional_Ordered_Resolution_Prover/document
20:15:21 Presenting document Functional_Ordered_Resolution_Prover/outline
20:15:21 Presenting theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover
20:15:21 Presenting theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover
20:15:21 Presenting theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
20:15:21 Presenting theory Functional_Ordered_Resolution_Prover.Executable_Subsumption
20:15:21 Presenting theory Functional_Ordered_Resolution_Prover.Executable_FO_Ordered_Resolution_Prover
20:15:22 Presenting Saturation_Framework ...
20:15:22 Presenting document Saturation_Framework/document
20:15:22 Presenting document Saturation_Framework/outline
20:15:22 Presenting theory Saturation_Framework.Calculus
20:15:22 Presenting theory Saturation_Framework.Intersection_Calculus
20:15:22 Presenting theory Saturation_Framework.Calculus_Variations
20:15:22 Presenting theory Saturation_Framework.Lifting_to_Non_Ground_Calculi
20:15:22 Presenting theory Saturation_Framework.Labeled_Lifting_to_Non_Ground_Calculi
20:15:22 Presenting theory Saturation_Framework.Given_Clause_Architectures
20:15:22 Presenting Saturation_Framework_Extensions ...
20:15:22 Presenting document Saturation_Framework_Extensions/document
20:15:22 Presenting document Saturation_Framework_Extensions/outline
20:15:22 Presenting theory Saturation_Framework_Extensions.Soundness
20:15:22 Presenting theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion
20:15:22 Presenting theory Saturation_Framework_Extensions.Clausal_Calculus
20:15:22 Presenting theory Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited
20:15:22 Presenting theory Saturation_Framework_Extensions.Given_Clause_Architectures_Revisited
20:15:23 Presenting POPLmark-deBruijn ...
20:15:23 Presenting document POPLmark-deBruijn/document
20:15:23 Presenting document POPLmark-deBruijn/outline
20:15:23 Presenting theory POPLmark-deBruijn.Basis
20:15:23 Presenting theory POPLmark-deBruijn.POPLmark
20:15:23 Presenting theory POPLmark-deBruijn.POPLmarkRecord
20:15:23 Presenting theory POPLmark-deBruijn.POPLmarkRecordCtxt
20:15:23 Presenting theory POPLmark-deBruijn.Execute
20:15:23 Presenting Pairing_Heap ...
20:15:23 Presenting document Pairing_Heap/document
20:15:23 Presenting document Pairing_Heap/outline
20:15:23 Presenting theory Pairing_Heap.Pairing_Heap_Tree
20:15:23 Presenting theory Pairing_Heap.Pairing_Heap_List1
20:15:23 Presenting theory Pairing_Heap.Pairing_Heap_List2
20:15:23 Presenting Password_Authentication_Protocol ...
20:15:23 Presenting document Password_Authentication_Protocol/document
20:15:23 Presenting document Password_Authentication_Protocol/outline
20:15:23 Presenting theory Password_Authentication_Protocol.Propaedeutics
20:15:23 Presenting theory Password_Authentication_Protocol.Protocol
20:15:25 Presenting Presburger-Automata ...
20:15:25 Presenting document Presburger-Automata/document
20:15:25 Presenting document Presburger-Automata/outline
20:15:25 Presenting theory Presburger-Automata.DFS
20:15:25 Presenting theory Presburger-Automata.Presburger_Automata
20:15:25 Presenting theory Presburger-Automata.Exec
20:15:27 Presenting Priority_Queue_Braun ...
20:15:27 Presenting document Priority_Queue_Braun/document
20:15:27 Presenting document Priority_Queue_Braun/outline
20:15:27 Presenting theory Priority_Queue_Braun.Priority_Queue_Braun
20:15:27 Presenting theory Priority_Queue_Braun.Priority_Queue_Braun2
20:15:27 Presenting theory Priority_Queue_Braun.Sorting_Braun
20:15:27 Presenting Program-Conflict-Analysis ...
20:15:27 Presenting document Program-Conflict-Analysis/document
20:15:27 Presenting document Program-Conflict-Analysis/outline
20:15:27 Presenting theory Program-Conflict-Analysis.Misc
20:15:27 Presenting theory Program-Conflict-Analysis.Interleave
20:15:27 Presenting theory Program-Conflict-Analysis.ConsInterleave
20:15:27 Presenting theory Program-Conflict-Analysis.AcquisitionHistory
20:15:27 Presenting theory Program-Conflict-Analysis.LTS
20:15:27 Presenting theory Program-Conflict-Analysis.ThreadTracking
20:15:27 Presenting theory Program-Conflict-Analysis.Flowgraph
20:15:27 Presenting theory Program-Conflict-Analysis.Semantics
20:15:27 Presenting theory Program-Conflict-Analysis.Normalization
20:15:27 Presenting theory Program-Conflict-Analysis.ConstraintSystems
20:15:27 Presenting theory Program-Conflict-Analysis.MainResult
20:15:28 Presenting Regression_Test_Selection ...
20:15:28 Presenting document Regression_Test_Selection/document
20:15:28 Presenting document Regression_Test_Selection/outline
20:15:28 Presenting theory Regression_Test_Selection.RTS_safe
20:15:28 Presenting theory Regression_Test_Selection.Semantics
20:15:28 Presenting theory Regression_Test_Selection.CollectionSemantics
20:15:28 Presenting theory Regression_Test_Selection.CollectionBasedRTS
20:15:28 Presenting theory Regression_Test_Selection.JVMSemantics
20:15:28 Presenting theory Regression_Test_Selection.ClassesChanged
20:15:28 Presenting theory Regression_Test_Selection.Subcls
20:15:28 Presenting theory Regression_Test_Selection.ClassesAbove
20:15:28 Presenting theory Regression_Test_Selection.JVMCollectionSemantics
20:15:28 Presenting theory Regression_Test_Selection.JVMExecStepInductive
20:15:28 Presenting theory Regression_Test_Selection.JVMCollectionBasedRTS
20:15:28 Presenting theory Regression_Test_Selection.RTS
20:15:29 Presenting Regular-Sets ...
20:15:29 Presenting document Regular-Sets/document
20:15:29 Presenting document Regular-Sets/outline
20:15:29 Presenting theory Regular-Sets.Regular_Set
20:15:29 Presenting theory Regular-Sets.Regular_Exp
20:15:29 Presenting theory Regular-Sets.NDerivative
20:15:29 Presenting theory Regular-Sets.Equivalence_Checking
20:15:29 Presenting theory Regular-Sets.Relation_Interpretation
20:15:29 Presenting theory Regular-Sets.Regexp_Method
20:15:29 Presenting theory Regular-Sets.Regexp_Constructions
20:15:29 Presenting theory Regular-Sets.Derivatives
20:15:29 Presenting theory Regular-Sets.pEquivalence_Checking
20:15:29 Presenting theory Regular-Sets.Regular_Exp2
20:15:29 Presenting theory Regular-Sets.Equivalence_Checking2
20:15:30 Presenting Posix-Lexing ...
20:15:30 Presenting document Posix-Lexing/document
20:15:30 Presenting document Posix-Lexing/outline
20:15:30 Presenting theory Posix-Lexing.Lexer
20:15:30 Presenting theory Posix-Lexing.Simplifying
20:15:30 Presenting Ribbon_Proofs ...
20:15:30 Presenting document Ribbon_Proofs/document
20:15:30 Presenting document Ribbon_Proofs/outline
20:15:30 Presenting theory Ribbon_Proofs.More_Finite_Map
20:15:30 Presenting theory Ribbon_Proofs.JHelper
20:15:30 Presenting theory Ribbon_Proofs.Proofchain
20:15:30 Presenting theory Ribbon_Proofs.Ribbons_Basic
20:15:30 Presenting theory Ribbon_Proofs.Ribbons_Interfaces
20:15:30 Presenting theory Ribbon_Proofs.Ribbons_Stratified
20:15:30 Presenting theory Ribbon_Proofs.Ribbons_Graphical
20:15:30 Presenting theory Ribbon_Proofs.Ribbons_Graphical_Soundness
20:15:30 Presenting Root_Balanced_Tree ...
20:15:30 Presenting document Root_Balanced_Tree/document
20:15:30 Presenting document Root_Balanced_Tree/outline
20:15:30 Presenting theory Root_Balanced_Tree.Time_Monad
20:15:30 Presenting theory Root_Balanced_Tree.Root_Balanced_Tree
20:15:30 Presenting theory Root_Balanced_Tree.Root_Balanced_Tree_Tab
20:15:31 Presenting SATSolverVerification ...
20:15:31 Presenting document SATSolverVerification/document
20:15:31 Presenting document SATSolverVerification/outline
20:15:31 Presenting theory SATSolverVerification.MoreList
20:15:31 Presenting theory SATSolverVerification.CNF
20:15:31 Presenting theory SATSolverVerification.Trail
20:15:31 Presenting theory SATSolverVerification.SatSolverVerification
20:15:31 Presenting theory SATSolverVerification.BasicDPLL
20:15:31 Presenting theory SATSolverVerification.NieuwenhuisOliverasTinelli
20:15:31 Presenting theory SATSolverVerification.KrsticGoel
20:15:31 Presenting theory SATSolverVerification.SatSolverCode
20:15:31 Presenting theory SATSolverVerification.AssertLiteral
20:15:31 Presenting theory SATSolverVerification.UnitPropagate
20:15:32 Presenting theory SATSolverVerification.Initialization
20:15:32 Presenting theory SATSolverVerification.ConflictAnalysis
20:15:32 Presenting theory SATSolverVerification.Decide
20:15:32 Presenting theory SATSolverVerification.SolveLoop
20:15:32 Presenting theory SATSolverVerification.FunctionalImplementation
20:15:34 Presenting Safe_OCL ...
20:15:34 Presenting document Safe_OCL/document
20:15:34 Presenting document Safe_OCL/outline
20:15:34 Presenting theory Safe_OCL.Errorable
20:15:34 Presenting theory Safe_OCL.Transitive_Closure_Ext
20:15:34 Presenting theory Safe_OCL.Finite_Map_Ext
20:15:34 Presenting theory Safe_OCL.Tuple
20:15:34 Presenting theory Safe_OCL.Object_Model
20:15:34 Presenting theory Safe_OCL.OCL_Basic_Types
20:15:34 Presenting theory Safe_OCL.OCL_Types
20:15:34 Presenting theory Safe_OCL.OCL_Syntax
20:15:34 Presenting theory Safe_OCL.OCL_Object_Model
20:15:35 Presenting theory Safe_OCL.OCL_Typing
20:15:35 Presenting theory Safe_OCL.OCL_Normalization
20:15:35 Presenting theory Safe_OCL.OCL_Examples
20:15:35 Presenting Selection_Heap_Sort ...
20:15:35 Presenting document Selection_Heap_Sort/document
20:15:35 Presenting document Selection_Heap_Sort/outline
20:15:35 Presenting theory Selection_Heap_Sort.Sort
20:15:35 Presenting theory Selection_Heap_Sort.RemoveMax
20:15:35 Presenting theory Selection_Heap_Sort.SelectionSort_Functional
20:15:35 Presenting theory Selection_Heap_Sort.Heap
20:15:35 Presenting theory Selection_Heap_Sort.HeapFunctional
20:15:35 Presenting theory Selection_Heap_Sort.HeapImperative
20:15:35 Presenting Separata ...
20:15:35 Presenting document Separata/document
20:15:35 Presenting document Separata/outline
20:15:35 Presenting theory Separata.Separata
20:15:35 Presenting Separation_Logic_Imperative_HOL ...
20:15:35 Presenting document Separation_Logic_Imperative_HOL/document
20:15:35 Presenting document Separation_Logic_Imperative_HOL/outline
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Syntax_Match
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Run
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Assertions
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Hoare_Triple
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Automation
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Sep_Main
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Imp_List_Spec
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.List_Seg
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Open_List
20:15:35 Presenting theory Separation_Logic_Imperative_HOL.Circ_List
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Imp_Map_Spec
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Hash_Table
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Hash_Map
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Hash_Map_Impl
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Imp_Set_Spec
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Hash_Set_Impl
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.To_List_GA
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Union_Find
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Idioms
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Default_Insts
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Array_Blit
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Array_Map_Impl
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Array_Set_Impl
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.From_List_GA
20:15:36 Presenting theory Separation_Logic_Imperative_HOL.Sep_Examples
20:15:36 Presenting Simplex ...
20:15:36 Presenting document Simplex/document
20:15:36 Presenting document Simplex/outline
20:15:36 Presenting theory Simplex.Simplex_Auxiliary
20:15:36 Presenting theory Simplex.Rel_Chain
20:15:36 Presenting theory Simplex.Simplex_Algebra
20:15:36 Presenting theory Simplex.Abstract_Linear_Poly
20:15:36 Presenting theory Simplex.Linear_Poly_Maps
20:15:36 Presenting theory Simplex.QDelta
20:15:36 Presenting theory Simplex.Simplex
20:15:36 Presenting theory Simplex.Simplex_Incremental
20:15:39 Presenting Farkas ...
20:15:39 Presenting document Farkas/document
20:15:39 Presenting document Farkas/outline
20:15:39 Presenting theory Farkas.Farkas
20:15:39 Presenting theory Farkas.Matrix_Farkas
20:15:39 Presenting theory Farkas.Simplex_for_Reals
20:15:40 Presenting Skew_Heap ...
20:15:40 Presenting document Skew_Heap/document
20:15:40 Presenting document Skew_Heap/outline
20:15:40 Presenting theory Skew_Heap.Skew_Heap
20:15:40 Presenting Splay_Tree ...
20:15:40 Presenting document Splay_Tree/document
20:15:40 Presenting document Splay_Tree/outline
20:15:40 Presenting theory Splay_Tree.Splay_Tree
20:15:40 Presenting theory Splay_Tree.Splay_Map
20:15:40 Presenting theory Splay_Tree.Splay_Heap
20:15:40 Presenting Stable_Matching ...
20:15:40 Presenting document Stable_Matching/document
20:15:40 Presenting document Stable_Matching/outline
20:15:40 Presenting theory Stable_Matching.Sotomayor
20:15:40 Presenting theory Stable_Matching.Basis
20:15:40 Presenting theory Stable_Matching.Choice_Functions
20:15:40 Presenting theory Stable_Matching.Contracts
20:15:40 Presenting theory Stable_Matching.COP
20:15:40 Presenting theory Stable_Matching.Bossiness
20:15:40 Presenting theory Stable_Matching.Strategic
20:15:41 Presenting SuperCalc ...
20:15:41 Presenting document SuperCalc/document
20:15:41 Presenting document SuperCalc/outline
20:15:41 Presenting theory SuperCalc.multisets_continued
20:15:41 Presenting theory SuperCalc.well_founded_continued
20:15:41 Presenting theory SuperCalc.terms
20:15:41 Presenting theory SuperCalc.equational_clausal_logic
20:15:41 Presenting theory SuperCalc.superposition
20:15:44 Presenting Tail_Recursive_Functions ...
20:15:44 Presenting document Tail_Recursive_Functions/document
20:15:44 Presenting document Tail_Recursive_Functions/outline
20:15:44 Presenting theory Tail_Recursive_Functions.Method
20:15:44 Presenting theory Tail_Recursive_Functions.CaseStudy1
20:15:44 Presenting theory Tail_Recursive_Functions.CaseStudy2
20:15:44 Presenting TortoiseHare ...
20:15:44 Presenting document TortoiseHare/document
20:15:44 Presenting document TortoiseHare/outline
20:15:44 Presenting theory TortoiseHare.Basis
20:15:44 Presenting theory TortoiseHare.TortoiseHare
20:15:44 Presenting theory TortoiseHare.Brent
20:15:44 Presenting Trie ...
20:15:44 Presenting document Trie/document
20:15:44 Presenting document Trie/outline
20:15:44 Presenting theory Trie.Trie
20:15:44 Presenting theory Trie.Tries
20:15:44 Presenting Twelvefold_Way ...
20:15:44 Presenting document Twelvefold_Way/document
20:15:44 Presenting document Twelvefold_Way/outline
20:15:44 Presenting theory Twelvefold_Way.Preliminaries
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Core
20:15:44 Presenting theory Twelvefold_Way.Equiv_Relations_on_Functions
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry1
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry2
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry4
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry5
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry6
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry7
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry8
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry9
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry3
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry10
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry11
20:15:44 Presenting theory Twelvefold_Way.Twelvefold_Way_Entry12
20:15:44 Presenting theory Twelvefold_Way.Card_Bijections
20:15:44 Presenting theory Twelvefold_Way.Card_Bijections_Direct
20:15:45 Presenting theory Twelvefold_Way.Twelvefold_Way
20:15:45 Presenting Vickrey_Clarke_Groves ...
20:15:45 Presenting document Vickrey_Clarke_Groves/document
20:15:45 Presenting document Vickrey_Clarke_Groves/outline
20:15:45 Presenting theory Vickrey_Clarke_Groves.SetUtils
20:15:45 Presenting theory Vickrey_Clarke_Groves.Partitions
20:15:45 Presenting theory Vickrey_Clarke_Groves.RelationOperators
20:15:45 Presenting theory Vickrey_Clarke_Groves.RelationProperties
20:15:45 Presenting theory Vickrey_Clarke_Groves.Argmax
20:15:45 Presenting theory Vickrey_Clarke_Groves.MiscTools
20:15:45 Presenting theory Vickrey_Clarke_Groves.StrictCombinatorialAuction
20:15:45 Presenting theory Vickrey_Clarke_Groves.Universes
20:15:45 Presenting theory Vickrey_Clarke_Groves.UniformTieBreaking
20:15:45 Presenting theory Vickrey_Clarke_Groves.CombinatorialAuction
20:15:45 Presenting theory Vickrey_Clarke_Groves.CombinatorialAuctionCodeExtraction
20:15:45 Presenting theory Vickrey_Clarke_Groves.FirstPrice
20:15:45 Presenting theory Vickrey_Clarke_Groves.CombinatorialAuctionExamples
20:15:46 Presenting WebAssembly ...
20:15:46 Presenting document WebAssembly/document
20:15:46 Presenting document WebAssembly/outline
20:15:46 Presenting theory WebAssembly.Wasm_Ast
20:15:46 Presenting theory WebAssembly.Wasm_Type_Abs
20:15:46 Presenting theory WebAssembly.Wasm_Base_Defs
20:15:46 Presenting theory WebAssembly.Wasm
20:15:46 Presenting theory WebAssembly.Wasm_Axioms
20:15:46 Presenting theory WebAssembly.Wasm_Properties_Aux
20:15:46 Presenting theory WebAssembly.Wasm_Properties
20:15:46 Presenting theory WebAssembly.Wasm_Soundness
20:15:46 Presenting theory WebAssembly.Wasm_Checker_Types
20:15:46 Presenting theory WebAssembly.Wasm_Checker
20:15:46 Presenting theory WebAssembly.Wasm_Checker_Properties
20:15:46 Presenting theory WebAssembly.Wasm_Interpreter
20:15:46 Presenting theory WebAssembly.Wasm_Interpreter_Properties
20:15:46 Presenting theory WebAssembly.Wasm_Checker_Printing
20:15:46 Presenting theory WebAssembly.Wasm_Interpreter_Printing
20:15:46 Presenting theory WebAssembly.Wasm_Type_Abs_Printing
20:15:46 Presenting theory WebAssembly.Wasm_Printing
20:15:46 Presenting theory WebAssembly.Wasm_Interpreter_Printing_Pure
20:15:47 Presenting Well_Quasi_Orders ...
20:15:47 Presenting document Well_Quasi_Orders/document
20:15:47 Presenting document Well_Quasi_Orders/outline
20:15:47 Presenting theory Well_Quasi_Orders.Infinite_Sequences
20:15:47 Presenting theory Well_Quasi_Orders.Minimal_Elements
20:15:47 Presenting theory Well_Quasi_Orders.Least_Enum
20:15:47 Presenting theory Well_Quasi_Orders.Almost_Full
20:15:47 Presenting theory Well_Quasi_Orders.Minimal_Bad_Sequences
20:15:47 Presenting theory Well_Quasi_Orders.Higman_OI
20:15:47 Presenting theory Well_Quasi_Orders.Almost_Full_Relations
20:15:47 Presenting theory Well_Quasi_Orders.Well_Quasi_Orders
20:15:47 Presenting theory Well_Quasi_Orders.Kruskal
20:15:47 Presenting theory Well_Quasi_Orders.Kruskal_Examples
20:15:47 Presenting theory Well_Quasi_Orders.Wqo_Instances
20:15:47 Presenting theory Well_Quasi_Orders.Multiset_Extension
20:15:47 Presenting theory Well_Quasi_Orders.Wqo_Multiset
20:15:48 Presenting XML ...
20:15:48 Presenting document XML/document
20:15:48 Presenting document XML/outline
20:15:48 Presenting theory XML.Xml
20:15:48 Presenting theory XML.Xmlt
20:15:48 Presenting CCS ...
20:15:48 Presenting document CCS/document
20:15:48 Presenting document CCS/outline
20:15:48 Presenting theory CCS.Agent
20:15:48 Presenting theory CCS.Tau_Chain
20:15:48 Presenting theory CCS.Weak_Cong_Semantics
20:15:48 Presenting theory CCS.Weak_Semantics
20:15:48 Presenting theory CCS.Strong_Sim
20:15:48 Presenting theory CCS.Weak_Sim
20:15:48 Presenting theory CCS.Weak_Cong_Sim
20:15:48 Presenting theory CCS.Strong_Sim_SC
20:15:48 Presenting theory CCS.Strong_Bisim
20:15:48 Presenting theory CCS.Strong_Sim_Pres
20:15:48 Presenting theory CCS.Strong_Bisim_Pres
20:15:48 Presenting theory CCS.Struct_Cong
20:15:48 Presenting theory CCS.Strong_Bisim_SC
20:15:48 Presenting theory CCS.Weak_Bisim
20:15:48 Presenting theory CCS.Weak_Cong
20:15:48 Presenting theory CCS.Weak_Sim_Pres
20:15:48 Presenting theory CCS.Weak_Bisim_Pres
20:15:48 Presenting theory CCS.Weak_Cong_Sim_Pres
20:15:48 Presenting theory CCS.Weak_Cong_Pres
20:15:48 Presenting Lam-ml-Normalization ...
20:15:48 Presenting document Lam-ml-Normalization/document
20:15:48 Presenting document Lam-ml-Normalization/outline
20:15:48 Presenting theory Lam-ml-Normalization.Lam_ml
20:15:49 Presenting Pi_Calculus ...
20:15:49 Presenting document Pi_Calculus/document
20:15:49 Presenting document Pi_Calculus/outline
20:15:49 Presenting theory Pi_Calculus.Agent
20:15:49 Presenting theory Pi_Calculus.Late_Semantics
20:15:49 Presenting theory Pi_Calculus.Late_Semantics1
20:15:49 Presenting theory Pi_Calculus.Rel
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Sim
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Bisim
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Bisim_Subst
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Sim_Pres
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Bisim_Pres
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Bisim_Subst_Pres
20:15:49 Presenting theory Pi_Calculus.Late_Tau_Chain
20:15:49 Presenting theory Pi_Calculus.Weak_Late_Step_Semantics
20:15:49 Presenting theory Pi_Calculus.Weak_Late_Semantics
20:15:49 Presenting theory Pi_Calculus.Weak_Late_Sim
20:15:49 Presenting theory Pi_Calculus.Weak_Late_Bisim
20:15:49 Presenting theory Pi_Calculus.Weak_Late_Step_Sim
20:15:49 Presenting theory Pi_Calculus.Weak_Late_Cong
20:15:49 Presenting theory Pi_Calculus.Weak_Late_Bisim_Subst
20:15:49 Presenting theory Pi_Calculus.Weak_Late_Cong_Subst
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Sim_SC
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Bisim_SC
20:15:49 Presenting theory Pi_Calculus.Strong_Late_Bisim_Subst_SC
20:15:50 Presenting theory Pi_Calculus.Weak_Late_Cong_Subst_SC
20:15:50 Presenting theory Pi_Calculus.Weak_Late_Step_Sim_Pres
20:15:50 Presenting theory Pi_Calculus.Weak_Late_Bisim_SC
20:15:50 Presenting theory Pi_Calculus.Weak_Late_Sim_Pres
20:15:50 Presenting theory Pi_Calculus.Weak_Late_Bisim_Pres
20:15:50 Presenting theory Pi_Calculus.Weak_Late_Cong_Pres
20:15:50 Presenting theory Pi_Calculus.Early_Semantics
20:15:51 Presenting theory Pi_Calculus.Strong_Early_Sim
20:15:51 Presenting theory Pi_Calculus.Strong_Early_Bisim
20:15:51 Presenting theory Pi_Calculus.Strong_Early_Bisim_Subst
20:15:51 Presenting theory Pi_Calculus.Strong_Early_Sim_Pres
20:15:51 Presenting theory Pi_Calculus.Strong_Early_Bisim_Pres
20:15:51 Presenting theory Pi_Calculus.Strong_Early_Bisim_Subst_Pres
20:15:51 Presenting theory Pi_Calculus.Early_Tau_Chain
20:15:51 Presenting theory Pi_Calculus.Weak_Early_Step_Semantics
20:15:51 Presenting theory Pi_Calculus.Weak_Early_Semantics
20:15:51 Presenting theory Pi_Calculus.Weak_Early_Sim
20:15:51 Presenting theory Pi_Calculus.Weak_Early_Bisim
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Step_Sim
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Cong
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Bisim_Subst
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Cong_Subst
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Step_Sim_Pres
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Sim_Pres
20:15:52 Presenting theory Pi_Calculus.Strong_Early_Late_Comp
20:15:52 Presenting theory Pi_Calculus.Strong_Early_Bisim_SC
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Bisim_SC
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Bisim_Pres
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Cong_Pres
20:15:52 Presenting theory Pi_Calculus.Weak_Early_Cong_Subst_Pres
20:15:52 Presenting theory Pi_Calculus.Strong_Late_Expansion_Law
20:15:52 Presenting theory Pi_Calculus.Strong_Late_Axiomatisation
20:15:54 Presenting Psi_Calculi ...
20:15:54 Presenting document Psi_Calculi/document
20:15:54 Presenting document Psi_Calculi/outline
20:15:54 Presenting theory Psi_Calculi.Chain
20:15:54 Presenting theory Psi_Calculi.Subst_Term
20:15:54 Presenting theory Psi_Calculi.Agent
20:15:54 Presenting theory Psi_Calculi.Frame
20:15:54 Presenting theory Psi_Calculi.Semantics
20:15:54 Presenting theory Psi_Calculi.Simulation
20:15:54 Presenting theory Psi_Calculi.Tau_Chain
20:15:54 Presenting theory Psi_Calculi.Weak_Simulation
20:15:54 Presenting theory Psi_Calculi.Weak_Stat_Imp
20:15:54 Presenting theory Psi_Calculi.Bisimulation
20:15:54 Presenting theory Psi_Calculi.Sim_Pres
20:15:55 Presenting theory Psi_Calculi.Bisim_Pres
20:15:55 Presenting theory Psi_Calculi.Sim_Struct_Cong
20:15:55 Presenting theory Psi_Calculi.Structural_Congruence
20:15:55 Presenting theory Psi_Calculi.Bisim_Struct_Cong
20:15:56 Presenting theory Psi_Calculi.Weak_Bisimulation
20:15:56 Presenting theory Psi_Calculi.Weak_Sim_Pres
20:15:56 Presenting theory Psi_Calculi.Weak_Stat_Imp_Pres
20:15:56 Presenting theory Psi_Calculi.Weak_Bisim_Pres
20:15:57 Presenting theory Psi_Calculi.Weak_Bisim_Struct_Cong
20:15:57 Presenting theory Psi_Calculi.Close_Subst
20:15:57 Presenting theory Psi_Calculi.Bisim_Subst
20:15:57 Presenting theory Psi_Calculi.Weak_Bisim_Subst
20:15:57 Presenting theory Psi_Calculi.Weakening
20:15:58 Presenting theory Psi_Calculi.Weaken_Transition
20:15:58 Presenting theory Psi_Calculi.Weaken_Stat_Imp
20:15:58 Presenting theory Psi_Calculi.Weaken_Simulation
20:15:58 Presenting theory Psi_Calculi.Weaken_Bisimulation
20:15:58 Presenting theory Psi_Calculi.Weak_Cong_Simulation
20:15:58 Presenting theory Psi_Calculi.Weak_Psi_Congruence
20:15:58 Presenting theory Psi_Calculi.Weak_Cong_Sim_Pres
20:15:58 Presenting theory Psi_Calculi.Weak_Cong_Pres
20:15:58 Presenting theory Psi_Calculi.Weak_Cong_Struct_Cong
20:15:59 Presenting theory Psi_Calculi.Weak_Congruence
20:15:59 Presenting theory Psi_Calculi.Tau
20:15:59 Presenting theory Psi_Calculi.Sum
20:15:59 Presenting theory Psi_Calculi.Tau_Sim
20:15:59 Presenting theory Psi_Calculi.Tau_Stat_Imp
20:16:00 Presenting theory Psi_Calculi.Tau_Laws_Weak
20:16:00 Presenting theory Psi_Calculi.Tau_Laws_No_Weak
20:16:05 Presenting SequentInvertibility ...
20:16:05 Presenting document SequentInvertibility/document
20:16:05 Presenting document SequentInvertibility/outline
20:16:05 Presenting theory SequentInvertibility.MultiSequents
20:16:05 Presenting theory SequentInvertibility.SingleSuccedent
20:16:05 Presenting theory SequentInvertibility.NominalSequents
20:16:05 Presenting theory SequentInvertibility.ModalSequents
20:16:05 Presenting theory SequentInvertibility.SRCTransforms
20:16:05 Presenting theory SequentInvertibility.SequentInvertibility
20:16:08 Presenting RIPEMD-160-SPARK ...
20:16:08 Presenting document RIPEMD-160-SPARK/document
20:16:08 Presenting document RIPEMD-160-SPARK/outline
20:16:08 Presenting theory RIPEMD-160-SPARK.RIPEMD_160_SPARK
20:16:08 Presenting CSP_RefTK ...
20:16:08 Presenting document CSP_RefTK/document
20:16:08 Presenting document CSP_RefTK/outline
20:16:08 Presenting theory CSP_RefTK.Introduction
20:16:08 Presenting theory CSP_RefTK.Assertions_ext
20:16:08 Presenting theory CSP_RefTK.Properties
20:16:08 Presenting theory CSP_RefTK.Fix_ind_ext
20:16:08 Presenting theory CSP_RefTK.Process_norm
20:16:08 Presenting theory CSP_RefTK.CopyBuffer_props
20:16:08 Presenting theory CSP_RefTK.DiningPhilosophers
20:16:08 Presenting theory CSP_RefTK.Conclusion
20:16:08 Presenting Circus ...
20:16:08 Presenting document Circus/document
20:16:08 Presenting document Circus/outline
20:16:08 Presenting theory Circus.Var
20:16:08 Presenting theory Circus.Relations
20:16:08 Presenting theory Circus.Designs
20:16:08 Presenting theory Circus.Reactive_Processes
20:16:08 Presenting theory Circus.CSP_Processes
20:16:08 Presenting theory Circus.Circus_Actions
20:16:08 Presenting theory Circus.Var_list
20:16:08 Presenting theory Circus.Denotational_Semantics
20:16:08 Presenting theory Circus.Circus_Syntax
20:16:08 Presenting theory Circus.Refinement
20:16:09 Presenting theory Circus.Refinement_Example
20:16:09 Presenting HOL-CSP ...
20:16:09 Presenting document HOL-CSP/document
20:16:09 Presenting document HOL-CSP/outline
20:16:09 Presenting theory HOL-CSP.Introduction
20:16:09 Presenting theory HOL-CSP.Process
20:16:09 Presenting theory HOL-CSP.Bot
20:16:09 Presenting theory HOL-CSP.Skip
20:16:09 Presenting theory HOL-CSP.Stop
20:16:09 Presenting theory HOL-CSP.Mprefix
20:16:09 Presenting theory HOL-CSP.Det
20:16:09 Presenting theory HOL-CSP.Ndet
20:16:09 Presenting theory HOL-CSP.Seq
20:16:09 Presenting theory HOL-CSP.Hide
20:16:09 Presenting theory HOL-CSP.Sync
20:16:09 Presenting theory HOL-CSP.Mndet
20:16:09 Presenting theory HOL-CSP.CSP
20:16:10 Presenting theory HOL-CSP.Assertions
20:16:10 Presenting theory HOL-CSP.Conclusion
20:16:10 Presenting theory HOL-CSP.CopyBuffer
20:16:11 Presenting PCF ...
20:16:11 Presenting document PCF/document
20:16:11 Presenting document PCF/outline
20:16:11 Presenting theory PCF.Basis
20:16:11 Presenting theory PCF.Logical_Relations
20:16:11 Presenting theory PCF.PCF
20:16:11 Presenting theory PCF.OpSem
20:16:11 Presenting theory PCF.Continuations
20:16:11 Presenting theory PCF.SmallStep
20:16:11 Presenting HOLCF-Prelude ...
20:16:11 Presenting document HOLCF-Prelude/document
20:16:11 Presenting document HOLCF-Prelude/outline
20:16:11 Presenting theory HOLCF-Prelude.HOLCF_Main
20:16:11 Presenting theory HOLCF-Prelude.Type_Classes
20:16:11 Presenting theory HOLCF-Prelude.Numeral_Cpo
20:16:11 Presenting theory HOLCF-Prelude.Data_Function
20:16:11 Presenting theory HOLCF-Prelude.Data_Bool
20:16:11 Presenting theory HOLCF-Prelude.Data_Tuple
20:16:11 Presenting theory HOLCF-Prelude.Data_Integer
20:16:11 Presenting theory HOLCF-Prelude.Data_Maybe
20:16:11 Presenting theory HOLCF-Prelude.Data_List
20:16:11 Presenting theory HOLCF-Prelude.Definedness
20:16:11 Presenting theory HOLCF-Prelude.List_Comprehension
20:16:12 Presenting theory HOLCF-Prelude.Num_Class
20:16:12 Presenting theory HOLCF-Prelude.HOLCF_Prelude
20:16:12 Presenting theory HOLCF-Prelude.Fibs
20:16:12 Presenting theory HOLCF-Prelude.Sieve_Primes
20:16:12 Presenting theory HOLCF-Prelude.GHC_Rewrite_Rules
20:16:12 Presenting theory HOLCF-Prelude.HLint
20:16:12 Presenting BirdKMP ...
20:16:12 Presenting document BirdKMP/document
20:16:12 Presenting document BirdKMP/outline
20:16:12 Presenting theory BirdKMP.HOLCF_ROOT
20:16:12 Presenting theory BirdKMP.Theory_Of_Lists
20:16:12 Presenting theory BirdKMP.KMP
20:16:13 Presenting Launchbury ...
20:16:13 Presenting document Launchbury/document
20:16:13 Presenting document Launchbury/outline
20:16:13 Presenting theory Launchbury.AList-Utils
20:16:13 Presenting theory Launchbury.HOLCF-Join
20:16:13 Presenting theory Launchbury.HOLCF-Join-Classes
20:16:13 Presenting theory Launchbury.Env
20:16:13 Presenting theory Launchbury.Pointwise
20:16:13 Presenting theory Launchbury.HOLCF-Utils
20:16:13 Presenting theory Launchbury.EvalHeap
20:16:13 Presenting theory Launchbury.Nominal-Utils
20:16:13 Presenting theory Launchbury.AList-Utils-Nominal
20:16:13 Presenting theory Launchbury.Nominal-HOLCF
20:16:13 Presenting theory Launchbury.Env-HOLCF
20:16:13 Presenting theory Launchbury.HasESem
20:16:13 Presenting theory Launchbury.Iterative
20:16:13 Presenting theory Launchbury.Env-Nominal
20:16:13 Presenting theory Launchbury.HeapSemantics
20:16:13 Presenting theory Launchbury.Vars
20:16:13 Presenting theory Launchbury.Terms
20:16:13 Presenting theory Launchbury.AbstractDenotational
20:16:13 Presenting theory Launchbury.Substitution
20:16:13 Presenting theory Launchbury.Abstract-Denotational-Props
20:16:13 Presenting theory Launchbury.Value
20:16:13 Presenting theory Launchbury.Value-Nominal
20:16:13 Presenting theory Launchbury.Denotational
20:16:13 Presenting theory Launchbury.Launchbury
20:16:13 Presenting theory Launchbury.CorrectnessOriginal
20:16:13 Presenting theory Launchbury.Mono-Nat-Fun
20:16:13 Presenting theory Launchbury.C
20:16:13 Presenting theory Launchbury.CValue
20:16:13 Presenting theory Launchbury.CValue-Nominal
20:16:13 Presenting theory Launchbury.HOLCF-Meet
20:16:13 Presenting theory Launchbury.C-Meet
20:16:13 Presenting theory Launchbury.C-restr
20:16:13 Presenting theory Launchbury.ResourcedDenotational
20:16:13 Presenting theory Launchbury.CorrectnessResourced
20:16:13 Presenting theory Launchbury.ResourcedAdequacy
20:16:13 Presenting theory Launchbury.ValueSimilarity
20:16:13 Presenting theory Launchbury.Denotational-Related
20:16:13 Presenting theory Launchbury.Adequacy
20:16:13 Presenting theory Launchbury.EverythingAdequacy
20:16:14 Presenting Call_Arity ...
20:16:14 Presenting document Call_Arity/document
20:16:14 Presenting document Call_Arity/outline
20:16:14 Presenting theory Call_Arity.BalancedTraces
20:16:14 Presenting theory Call_Arity.SestoftConf
20:16:14 Presenting theory Call_Arity.Sestoft
20:16:14 Presenting theory Call_Arity.SestoftCorrect
20:16:14 Presenting theory Call_Arity.Arity
20:16:14 Presenting theory Call_Arity.AEnv
20:16:14 Presenting theory Call_Arity.Arity-Nominal
20:16:14 Presenting theory Call_Arity.ArityAnalysisSig
20:16:14 Presenting theory Call_Arity.ArityAnalysisAbinds
20:16:14 Presenting theory Call_Arity.ArityAnalysisSpec
20:16:14 Presenting theory Call_Arity.TrivialArityAnal
20:16:14 Presenting theory Call_Arity.Cardinality-Domain
20:16:14 Presenting theory Call_Arity.CardinalityAnalysisSig
20:16:14 Presenting theory Call_Arity.ConstOn
20:16:14 Presenting theory Call_Arity.CardinalityAnalysisSpec
20:16:14 Presenting theory Call_Arity.ArityAnalysisStack
20:16:14 Presenting theory Call_Arity.NoCardinalityAnalysis
20:16:14 Presenting theory Call_Arity.TransformTools
20:16:14 Presenting theory Call_Arity.AbstractTransform
20:16:14 Presenting theory Call_Arity.EtaExpansion
20:16:14 Presenting theory Call_Arity.EtaExpansionSafe
20:16:14 Presenting theory Call_Arity.ArityStack
20:16:14 Presenting theory Call_Arity.ArityEtaExpansion
20:16:14 Presenting theory Call_Arity.ArityEtaExpansionSafe
20:16:14 Presenting theory Call_Arity.ArityTransform
20:16:14 Presenting theory Call_Arity.ArityConsistent
20:16:14 Presenting theory Call_Arity.ArityTransformSafe
20:16:14 Presenting theory Call_Arity.Set-Cpo
20:16:14 Presenting theory Call_Arity.Env-Set-Cpo
20:16:14 Presenting theory Call_Arity.CoCallGraph
20:16:14 Presenting theory Call_Arity.CoCallAnalysisSig
20:16:14 Presenting theory Call_Arity.AList-Utils-HOLCF
20:16:14 Presenting theory Call_Arity.CoCallGraph-Nominal
20:16:14 Presenting theory Call_Arity.CoCallAnalysisBinds
20:16:14 Presenting theory Call_Arity.ArityAnalysisFix
20:16:14 Presenting theory Call_Arity.CoCallFix
20:16:14 Presenting theory Call_Arity.CoCallAnalysisImpl
20:16:14 Presenting theory Call_Arity.CallArityEnd2End
20:16:14 Presenting theory Call_Arity.SestoftGC
20:16:14 Presenting theory Call_Arity.CardArityTransformSafe
20:16:14 Presenting theory Call_Arity.CoCallAritySig
20:16:14 Presenting theory Call_Arity.CoCallAnalysisSpec
20:16:15 Presenting theory Call_Arity.ArityAnalysisFixProps
20:16:15 Presenting theory Call_Arity.CoCallImplSafe
20:16:15 Presenting theory Call_Arity.List-Interleavings
20:16:15 Presenting theory Call_Arity.TTree
20:16:15 Presenting theory Call_Arity.TTree-HOLCF
20:16:15 Presenting theory Call_Arity.AnalBinds
20:16:15 Presenting theory Call_Arity.TTreeAnalysisSig
20:16:15 Presenting theory Call_Arity.CoCallGraph-TTree
20:16:15 Presenting theory Call_Arity.CoCallImplTTree
20:16:15 Presenting theory Call_Arity.Cardinality-Domain-Lists
20:16:15 Presenting theory Call_Arity.TTreeAnalysisSpec
20:16:15 Presenting theory Call_Arity.CoCallImplTTreeSafe
20:16:15 Presenting theory Call_Arity.TTreeImplCardinality
20:16:15 Presenting theory Call_Arity.TTreeImplCardinalitySafe
20:16:15 Presenting theory Call_Arity.CallArityEnd2EndSafe
20:16:15 Presenting theory Call_Arity.ArityAnalysisCorrDenotational
20:16:16 Presenting Shivers-CFA ...
20:16:16 Presenting document Shivers-CFA/document
20:16:16 Presenting document Shivers-CFA/outline
20:16:16 Presenting theory Shivers-CFA.HOLCFUtils
20:16:16 Presenting theory Shivers-CFA.CPSScheme
20:16:16 Presenting theory Shivers-CFA.Eval
20:16:16 Presenting theory Shivers-CFA.Utils
20:16:16 Presenting theory Shivers-CFA.SetMap
20:16:16 Presenting theory Shivers-CFA.AbsCF
20:16:16 Presenting theory Shivers-CFA.ExCF
20:16:16 Presenting theory Shivers-CFA.AbsCFCorrect
20:16:16 Presenting theory Shivers-CFA.ExCFSV
20:16:16 Presenting theory Shivers-CFA.Computability
20:16:16 Presenting theory Shivers-CFA.FixTransform
20:16:16 Presenting theory Shivers-CFA.CPSUtils
20:16:16 Presenting theory Shivers-CFA.MapSets
20:16:16 Presenting theory Shivers-CFA.AbsCFComp
20:16:16 Presenting Stream-Fusion ...
20:16:16 Presenting document Stream-Fusion/document
20:16:16 Presenting document Stream-Fusion/outline
20:16:16 Presenting theory Stream-Fusion.LazyList
20:16:16 Presenting theory Stream-Fusion.Stream
20:16:16 Presenting theory Stream-Fusion.StreamFusion
20:16:17 Presenting Tycon ...
20:16:17 Presenting document Tycon/document
20:16:17 Presenting document Tycon/outline
20:16:17 Presenting theory Tycon.TypeApp
20:16:17 Presenting theory Tycon.Coerce
20:16:17 Presenting theory Tycon.Functor
20:16:17 Presenting theory Tycon.Monad
20:16:17 Presenting theory Tycon.Monad_Zero
20:16:17 Presenting theory Tycon.Monad_Plus
20:16:17 Presenting theory Tycon.Monad_Zero_Plus
20:16:17 Presenting theory Tycon.Lazy_List_Monad
20:16:17 Presenting theory Tycon.Maybe_Monad
20:16:17 Presenting theory Tycon.Error_Monad
20:16:17 Presenting theory Tycon.Writer_Monad
20:16:17 Presenting theory Tycon.Binary_Tree_Monad
20:16:17 Presenting theory Tycon.Lift_Monad
20:16:17 Presenting theory Tycon.Resumption_Transformer
20:16:17 Presenting theory Tycon.State_Transformer
20:16:17 Presenting theory Tycon.Error_Transformer
20:16:17 Presenting theory Tycon.Writer_Transformer
20:16:17 Presenting theory Tycon.Monad_Transformer
20:16:17 Presenting file "tycondef.ML"
20:16:17 Presenting WorkerWrapper ...
20:16:17 Presenting document WorkerWrapper/document
20:16:17 Presenting document WorkerWrapper/outline
20:16:17 Presenting theory WorkerWrapper.Nats
20:16:17 Presenting theory WorkerWrapper.LList
20:16:17 Presenting theory WorkerWrapper.Maybe
20:16:17 Presenting theory WorkerWrapper.FixedPointTheorems
20:16:17 Presenting theory WorkerWrapper.WorkerWrapper
20:16:17 Presenting theory WorkerWrapper.CounterExample
20:16:17 Presenting theory WorkerWrapper.WorkerWrapperNew
20:16:17 Presenting theory WorkerWrapper.Accumulator
20:16:17 Presenting theory WorkerWrapper.UnboxedNats
20:16:17 Presenting theory WorkerWrapper.Streams
20:16:17 Presenting theory WorkerWrapper.Continuations
20:16:17 Presenting theory WorkerWrapper.Backtracking
20:16:17 Presenting theory WorkerWrapper.Nub
20:16:17 Presenting theory WorkerWrapper.Last
20:16:18 Presenting Heard_Of ...
20:16:18 Presenting document Heard_Of/document
20:16:18 Presenting document Heard_Of/outline
20:16:18 Presenting theory Heard_Of.HOModel
20:16:18 Presenting theory Heard_Of.Reduction
20:16:18 Presenting theory Heard_Of.Majorities
20:16:18 Presenting theory Heard_Of.OneThirdRuleDefs
20:16:18 Presenting theory Heard_Of.OneThirdRuleProof
20:16:18 Presenting theory Heard_Of.UvDefs
20:16:18 Presenting theory Heard_Of.UvProof
20:16:18 Presenting theory Heard_Of.LastVotingDefs
20:16:18 Presenting theory Heard_Of.LastVotingProof
20:16:18 Presenting theory Heard_Of.UteDefs
20:16:18 Presenting theory Heard_Of.UteProof
20:16:18 Presenting theory Heard_Of.AteDefs
20:16:18 Presenting theory Heard_Of.AteProof
20:16:18 Presenting theory Heard_Of.EigbyzDefs
20:16:18 Presenting theory Heard_Of.EigbyzProof
20:16:19 Presenting Hello_World ...
20:16:19 Presenting document Hello_World/document
20:16:19 Presenting document Hello_World/outline
20:16:19 Presenting theory Hello_World.IO
20:16:19 Presenting theory Hello_World.HelloWorld
20:16:19 Presenting theory Hello_World.HelloWorld_Proof
20:16:19 Presenting theory Hello_World.RunningCodeFromIsabelle
20:16:19 Presenting Higher_Order_Terms ...
20:16:19 Presenting document Higher_Order_Terms/document
20:16:19 Presenting document Higher_Order_Terms/outline
20:16:19 Presenting theory Higher_Order_Terms.Term_Utils
20:16:19 Presenting theory Higher_Order_Terms.Find_First
20:16:19 Presenting theory Higher_Order_Terms.Name
20:16:19 Presenting theory Higher_Order_Terms.Fresh_Monad
20:16:19 Presenting theory Higher_Order_Terms.Fresh_Class
20:16:19 Presenting theory Higher_Order_Terms.Term_Class
20:16:19 Presenting theory Higher_Order_Terms.Term
20:16:19 Presenting theory Higher_Order_Terms.Pats
20:16:19 Presenting theory Higher_Order_Terms.Nterm
20:16:19 Presenting theory Higher_Order_Terms.Term_to_Nterm
20:16:19 Presenting theory Higher_Order_Terms.Unification_Compat
20:16:19 Presenting theory Higher_Order_Terms.Lambda_Free_Compat
20:16:19 Presenting Hoare_Time ...
20:16:19 Presenting document Hoare_Time/document
20:16:19 Presenting document Hoare_Time/outline
20:16:19 Presenting theory Hoare_Time.AExp
20:16:19 Presenting theory Hoare_Time.BExp
20:16:19 Presenting theory Hoare_Time.Com
20:16:19 Presenting theory Hoare_Time.Big_Step
20:16:19 Presenting theory Hoare_Time.Big_StepT
20:16:19 Presenting theory Hoare_Time.Nielson_Hoare
20:16:19 Presenting theory Hoare_Time.Nielson_VCG
20:16:19 Presenting theory Hoare_Time.Vars
20:16:19 Presenting theory Hoare_Time.Nielson_VCGi
20:16:19 Presenting theory Hoare_Time.Nielson_VCGi_complete
20:16:19 Presenting theory Hoare_Time.Nielson_Examples
20:16:19 Presenting theory Hoare_Time.Nielson_Sqrt
20:16:19 Presenting theory Hoare_Time.Quant_Hoare
20:16:19 Presenting theory Hoare_Time.Quant_VCG
20:16:20 Presenting theory Hoare_Time.Quant_Examples
20:16:20 Presenting theory Hoare_Time.QuantK_Hoare
20:16:20 Presenting theory Hoare_Time.QuantK_VCG
20:16:20 Presenting theory Hoare_Time.QuantK_Examples
20:16:20 Presenting theory Hoare_Time.QuantK_Sqrt
20:16:20 Presenting theory Hoare_Time.Partial_Evaluation
20:16:20 Presenting theory Hoare_Time.Product_Separation_Algebra
20:16:20 Presenting theory Hoare_Time.Sep_Algebra_Add
20:16:20 Presenting theory Hoare_Time.Big_StepT_Partial
20:16:20 Presenting theory Hoare_Time.SepLog_Hoare
20:16:20 Presenting theory Hoare_Time.SepLog_Examples
20:16:20 Presenting theory Hoare_Time.SepLogK_Hoare
20:16:20 Presenting theory Hoare_Time.SepLogK_VCG
20:16:21 Presenting theory Hoare_Time.Discussion
20:16:21 Presenting theory Hoare_Time.DiscussionO
20:16:21 Presenting theory Hoare_Time.Hoare_Time
20:16:22 Presenting Hood_Melville_Queue ...
20:16:22 Presenting document Hood_Melville_Queue/document
20:16:22 Presenting document Hood_Melville_Queue/outline
20:16:22 Presenting theory Hood_Melville_Queue.Hood_Melville_Queue
20:16:22 Presenting HotelKeyCards ...
20:16:22 Presenting document HotelKeyCards/document
20:16:22 Presenting document HotelKeyCards/outline
20:16:22 Presenting theory HotelKeyCards.Notation
20:16:22 Presenting theory HotelKeyCards.Basis
20:16:22 Presenting theory HotelKeyCards.State
20:16:22 Presenting theory HotelKeyCards.NewCard
20:16:22 Presenting theory HotelKeyCards.Trace
20:16:22 Presenting theory HotelKeyCards.Equivalence
20:16:22 Presenting Huffman ...
20:16:22 Presenting document Huffman/document
20:16:22 Presenting document Huffman/outline
20:16:22 Presenting theory Huffman.Huffman
20:16:23 Presenting Hybrid_Logic ...
20:16:23 Presenting document Hybrid_Logic/document
20:16:23 Presenting document Hybrid_Logic/outline
20:16:23 Presenting theory Hybrid_Logic.Hybrid_Logic
20:16:24 Presenting Hybrid_Multi_Lane_Spatial_Logic ...
20:16:24 Presenting document Hybrid_Multi_Lane_Spatial_Logic/document
20:16:24 Presenting document Hybrid_Multi_Lane_Spatial_Logic/outline
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.NatInt
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.RealInt
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Cars
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Traffic
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Views
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Restriction
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Move
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Sensors
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Length
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Perfect_Sensors
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL_Perfect
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Safety_Perfect
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Regular_Sensors
20:16:24 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL_Regular
20:16:25 Presenting theory Hybrid_Multi_Lane_Spatial_Logic.Safety_Regular
20:16:25 Presenting IFC_Tracking ...
20:16:25 Presenting document IFC_Tracking/document
20:16:25 Presenting document IFC_Tracking/outline
20:16:25 Presenting theory IFC_Tracking.IFC
20:16:25 Presenting theory IFC_Tracking.PDG
20:16:26 Presenting IMP2 ...
20:16:26 Presenting document IMP2/document
20:16:26 Presenting document IMP2/outline
20:16:26 Presenting theory IMP2.IMP2_Aux_Lemmas
20:16:26 Presenting theory IMP2.IMP2_Utils
20:16:26 Presenting theory IMP2.Named_Simpsets
20:16:26 Presenting theory IMP2.Subgoal_Focus_Some
20:16:26 Presenting theory IMP2.Syntax
20:16:26 Presenting theory IMP2.Semantics
20:16:26 Presenting theory IMP2.Annotated_Syntax
20:16:26 Presenting theory IMP2.IMP2_Basic_Simpset
20:16:26 Presenting theory IMP2.Parser
20:16:27 Presenting theory IMP2.IMP2_Basic_Decls
20:16:27 Presenting theory IMP2.IMP2_Program_Analysis
20:16:27 Presenting theory IMP2.IMP2_Var_Postprocessor
20:16:27 Presenting theory IMP2.IMP2_Var_Abs
20:16:27 Presenting theory IMP2.IMP2_VCG
20:16:27 Presenting theory IMP2.IMP2_Specification
20:16:27 Presenting theory IMP2.IMP2
20:16:27 Presenting file "subgoal_focus_some.ML"
20:16:27 Presenting theory IMP2.Quickstart_Guide
20:16:27 Presenting theory IMP2.IMP2_from_IMP
20:16:27 Presenting theory IMP2.Examples
20:16:28 Presenting file "named_simpsets.ML"
20:16:28 Presenting IMP2_Binary_Heap ...
20:16:28 Presenting document IMP2_Binary_Heap/document
20:16:28 Presenting document IMP2_Binary_Heap/outline
20:16:28 Presenting theory IMP2_Binary_Heap.IMP2_Binary_Heap
20:16:28 Presenting IMP_Compiler ...
20:16:28 Presenting document IMP_Compiler/document
20:16:28 Presenting document IMP_Compiler/outline
20:16:28 Presenting theory IMP_Compiler.Compiler
20:16:28 Presenting theory IMP_Compiler.Compiler2
20:16:28 Presenting Impossible_Geometry ...
20:16:28 Presenting document Impossible_Geometry/document
20:16:28 Presenting document Impossible_Geometry/outline
20:16:28 Presenting theory Impossible_Geometry.Impossible_Geometry
20:16:29 Presenting Inductive_Confidentiality ...
20:16:29 Presenting document Inductive_Confidentiality/document
20:16:29 Presenting document Inductive_Confidentiality/outline
20:16:29 Presenting theory Inductive_Confidentiality.Message
20:16:29 Presenting theory Inductive_Confidentiality.Event
20:16:29 Presenting theory Inductive_Confidentiality.Public
20:16:29 Presenting theory Inductive_Confidentiality.NS_Public_Bad
20:16:29 Presenting theory Inductive_Confidentiality.ConfidentialityDY
20:16:29 Presenting theory Inductive_Confidentiality.MessageGA
20:16:29 Presenting theory Inductive_Confidentiality.EventGA
20:16:29 Presenting theory Inductive_Confidentiality.PublicGA
20:16:29 Presenting theory Inductive_Confidentiality.NS_Public_Bad_GA
20:16:29 Presenting theory Inductive_Confidentiality.ConfidentialityGA
20:16:29 Presenting theory Inductive_Confidentiality.Knowledge
20:16:29 Presenting Inductive_Inference ...
20:16:29 Presenting document Inductive_Inference/document
20:16:29 Presenting document Inductive_Inference/outline
20:16:29 Presenting theory Inductive_Inference.Partial_Recursive
20:16:29 Presenting theory Inductive_Inference.Universal
20:16:29 Presenting theory Inductive_Inference.Standard_Results
20:16:29 Presenting theory Inductive_Inference.Inductive_Inference_Basics
20:16:29 Presenting theory Inductive_Inference.CP_FIN_NUM
20:16:29 Presenting theory Inductive_Inference.CONS_LIM
20:16:29 Presenting theory Inductive_Inference.Lemma_R
20:16:29 Presenting theory Inductive_Inference.LIM_BC
20:16:29 Presenting theory Inductive_Inference.TOTAL_CONS
20:16:30 Presenting theory Inductive_Inference.R1_BC
20:16:31 Presenting theory Inductive_Inference.Union
20:16:32 Presenting InfPathElimination ...
20:16:32 Presenting document InfPathElimination/document
20:16:32 Presenting document InfPathElimination/outline
20:16:32 Presenting theory InfPathElimination.Graph
20:16:32 Presenting theory InfPathElimination.Aexp
20:16:32 Presenting theory InfPathElimination.Bexp
20:16:32 Presenting theory InfPathElimination.Labels
20:16:32 Presenting theory InfPathElimination.Store
20:16:32 Presenting theory InfPathElimination.Conf
20:16:32 Presenting theory InfPathElimination.SymExec
20:16:32 Presenting theory InfPathElimination.LTS
20:16:32 Presenting theory InfPathElimination.SubRel
20:16:32 Presenting theory InfPathElimination.ArcExt
20:16:32 Presenting theory InfPathElimination.SubExt
20:16:32 Presenting theory InfPathElimination.RB
20:16:33 Presenting Intro_Dest_Elim ...
20:16:33 Presenting document Intro_Dest_Elim/document
20:16:33 Presenting document Intro_Dest_Elim/outline
20:16:33 Presenting theory Intro_Dest_Elim.IDE_Tools
20:16:33 Presenting theory Intro_Dest_Elim.IHOL_IDE
20:16:33 Presenting theory Intro_Dest_Elim.Reference_Prerequisites
20:16:33 Presenting theory Intro_Dest_Elim.IDE_Reference
20:16:33 Presenting file "IDE_Utilities.ML"
20:16:33 Presenting file "IDE.ML"
20:16:33 Presenting file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
20:16:33 Presenting IsaGeoCoq ...
20:16:33 Presenting document IsaGeoCoq/document
20:16:33 Presenting document IsaGeoCoq/outline
20:16:33 Presenting theory IsaGeoCoq.Tarski_Neutral
20:16:36 Presenting Isabelle_C ...
20:16:36 Presenting document Isabelle_C/document
20:16:36 Presenting document Isabelle_C/outline
20:16:36 Presenting theory Isabelle_C.C_Lexer_Language
20:16:36 Presenting theory Isabelle_C.C_Ast
20:16:36 Presenting theory Isabelle_C.C_Environment
20:16:36 Presenting theory Isabelle_C.C_Parser_Language
20:16:36 Presenting theory Isabelle_C.C_Lexer_Annotation
20:16:36 Presenting theory Isabelle_C.C_Parser_Annotation
20:16:36 Presenting theory Isabelle_C.C_Eval
20:16:36 Presenting theory Isabelle_C.C_Command
20:16:36 Presenting theory Isabelle_C.C_Document
20:16:37 Presenting theory Isabelle_C.C_Main
20:16:37 Presenting theory Isabelle_C.C0
20:16:37 Presenting theory Isabelle_C.C1
20:16:37 Presenting theory Isabelle_C.C2
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/argument_scope.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/atomic_parenthesis.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.ok.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/block_scope.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/char-literal-printing.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/c-namespace.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/control-scope.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/dangling_else.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/declarators.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/designator.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/enum.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/enum_constant_visibility.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/enum_shadows_typedef.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/enum-trick.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/expressions.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/function-decls.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/local_scope.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/local_typedef.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/long-long-struct.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/namespaces.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/no_local_scope.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/parameter_declaration_ambiguity.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/parameter_declaration_ambiguity.test.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/statements.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/struct-recursion.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/typedef_star.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/types.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/variable_star.c"
20:16:37 Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.fail.c"
20:16:37 Presenting theory Isabelle_C.C_paper
20:16:37 Presenting theory Isabelle_C.C_Appendices
20:16:38 Presenting theory Isabelle_C.README
20:16:43 Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/base.sig"
20:16:43 Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/join.sml"
20:16:43 Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/lrtable.sml"
20:16:43 Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/stream.sml"
20:16:43 Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/parser1.sml"
20:16:43 Presenting file "$AFP/Isabelle_C/C11-FrontEnd/generated/c_grammar_fun.grm.sig"
20:16:43 Presenting file "$AFP/Isabelle_C/C11-FrontEnd/generated/c_grammar_fun.grm.sml"
20:16:49 Presenting file "$AFP/Isabelle_C/C11-FrontEnd/generated/c_ast.ML"
20:16:51 Presenting Jacobson_Basic_Algebra ...
20:16:51 Presenting document Jacobson_Basic_Algebra/document
20:16:51 Presenting document Jacobson_Basic_Algebra/outline
20:16:51 Presenting theory Jacobson_Basic_Algebra.Set_Theory
20:16:51 Presenting theory Jacobson_Basic_Algebra.Group_Theory
20:16:51 Presenting theory Jacobson_Basic_Algebra.Ring_Theory
20:16:51 Presenting JiveDataStoreModel ...
20:16:51 Presenting document JiveDataStoreModel/document
20:16:51 Presenting document JiveDataStoreModel/outline
20:16:51 Presenting theory JiveDataStoreModel.TypeIds
20:16:51 Presenting theory JiveDataStoreModel.JavaType
20:16:51 Presenting theory JiveDataStoreModel.DirectSubtypes
20:16:51 Presenting theory JiveDataStoreModel.Subtype
20:16:51 Presenting theory JiveDataStoreModel.Attributes
20:16:51 Presenting theory JiveDataStoreModel.AttributesIndep
20:16:51 Presenting theory JiveDataStoreModel.Value
20:16:51 Presenting theory JiveDataStoreModel.Location
20:16:51 Presenting theory JiveDataStoreModel.Store
20:16:51 Presenting theory JiveDataStoreModel.StoreProperties
20:16:51 Presenting theory JiveDataStoreModel.JML
20:16:51 Presenting theory JiveDataStoreModel.UnivSpec
20:16:52 Presenting KAD ...
20:16:52 Presenting document KAD/document
20:16:52 Presenting document KAD/outline
20:16:52 Presenting theory KAD.Domain_Semiring
20:16:52 Presenting theory KAD.Antidomain_Semiring
20:16:52 Presenting theory KAD.Range_Semiring
20:16:52 Presenting theory KAD.Modal_Kleene_Algebra
20:16:52 Presenting theory KAD.Modal_Kleene_Algebra_Models
20:16:52 Presenting theory KAD.Modal_Kleene_Algebra_Applications
20:16:52 Presenting Key_Agreement_Strong_Adversaries ...
20:16:52 Presenting document Key_Agreement_Strong_Adversaries/document
20:16:52 Presenting document Key_Agreement_Strong_Adversaries/outline
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Infra
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Refinement
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Messages
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Message_derivation
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.IK
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Secrecy
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.AuthenticationN
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.AuthenticationI
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Runs
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Channels
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Payloads
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Implem
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Implem_lemmas
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Implem_symmetric
20:16:52 Presenting theory Key_Agreement_Strong_Adversaries.Implem_asymmetric
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.pfslvl1
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.pfslvl2
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.pfslvl3
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.pfslvl3_asymmetric
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.pfslvl3_symmetric
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.dhlvl1
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.dhlvl2
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.dhlvl3
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.dhlvl3_asymmetric
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.dhlvl3_symmetric
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.sklvl1
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.sklvl2
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.sklvl3
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.sklvl3_asymmetric
20:16:53 Presenting theory Key_Agreement_Strong_Adversaries.sklvl3_symmetric
20:16:54 Presenting Kleene_Algebra ...
20:16:54 Presenting document Kleene_Algebra/document
20:16:54 Presenting document Kleene_Algebra/outline
20:16:54 Presenting theory Kleene_Algebra.Signatures
20:16:54 Presenting theory Kleene_Algebra.Dioid
20:16:54 Presenting theory Kleene_Algebra.Dioid_Models
20:16:54 Presenting theory Kleene_Algebra.Matrix
20:16:54 Presenting theory Kleene_Algebra.Conway
20:16:54 Presenting theory Kleene_Algebra.Kleene_Algebra
20:16:54 Presenting theory Kleene_Algebra.Kleene_Algebra_Models
20:16:54 Presenting theory Kleene_Algebra.Omega_Algebra
20:16:54 Presenting theory Kleene_Algebra.Omega_Algebra_Models
20:16:54 Presenting theory Kleene_Algebra.DRA
20:16:54 Presenting theory Kleene_Algebra.PHL_KA
20:16:54 Presenting theory Kleene_Algebra.PHL_DRA
20:16:54 Presenting theory Kleene_Algebra.Finite_Suprema
20:16:54 Presenting theory Kleene_Algebra.Formal_Power_Series
20:16:54 Presenting theory Kleene_Algebra.Inf_Matrix
20:16:54 Presenting KAT_and_DRA ...
20:16:54 Presenting document KAT_and_DRA/document
20:16:54 Presenting document KAT_and_DRA/outline
20:16:54 Presenting theory KAT_and_DRA.Test_Dioid
20:16:54 Presenting theory KAT_and_DRA.Conway_Tests
20:16:54 Presenting theory KAT_and_DRA.KAT
20:16:54 Presenting theory KAT_and_DRA.DRAT
20:16:54 Presenting theory KAT_and_DRA.DRA_Models
20:16:54 Presenting theory KAT_and_DRA.KAT_Models
20:16:54 Presenting theory KAT_and_DRA.FolkTheorem
20:16:54 Presenting theory KAT_and_DRA.PHL_KAT
20:16:54 Presenting theory KAT_and_DRA.PHL_DRAT
20:16:54 Presenting theory KAT_and_DRA.KAT2
20:16:54 Presenting theory KAT_and_DRA.DRAT2
20:16:55 Presenting Algebraic_VCs ...
20:16:55 Presenting document Algebraic_VCs/document
20:16:55 Presenting document Algebraic_VCs/outline
20:16:55 Presenting theory Algebraic_VCs.VC_KAT_scratch
20:16:55 Presenting theory Algebraic_VCs.VC_KAD_scratch
20:16:55 Presenting theory Algebraic_VCs.P2S2R
20:16:55 Presenting theory Algebraic_VCs.VC_KAT
20:16:55 Presenting theory Algebraic_VCs.VC_KAT_Examples
20:16:55 Presenting theory Algebraic_VCs.VC_KAT_Examples2
20:16:55 Presenting theory Algebraic_VCs.RKAT
20:16:55 Presenting theory Algebraic_VCs.RKAT_Models
20:16:55 Presenting theory Algebraic_VCs.VC_RKAT
20:16:55 Presenting theory Algebraic_VCs.VC_RKAT_Examples
20:16:55 Presenting theory Algebraic_VCs.VC_KAD
20:16:55 Presenting theory Algebraic_VCs.VC_KAD_Examples
20:16:55 Presenting theory Algebraic_VCs.VC_KAD_Examples2
20:16:55 Presenting theory Algebraic_VCs.VC_KAD_dual
20:16:55 Presenting theory Algebraic_VCs.VC_KAD_dual_Examples
20:16:55 Presenting theory Algebraic_VCs.VC_KAD_wf
20:16:55 Presenting theory Algebraic_VCs.VC_KAD_wf_Examples
20:16:55 Presenting theory Algebraic_VCs.Path_Model_Example
20:16:55 Presenting theory Algebraic_VCs.Pointer_Examples
20:16:55 Presenting theory Algebraic_VCs.KAD_is_KAT
20:16:55 Presenting theory Algebraic_VCs.Domain_Quantale
20:16:55 Presenting Multirelations ...
20:16:55 Presenting document Multirelations/document
20:16:55 Presenting document Multirelations/outline
20:16:55 Presenting theory Multirelations.C_Algebras
20:16:55 Presenting theory Multirelations.Multirelations
20:16:56 Presenting Regular_Algebras ...
20:16:56 Presenting document Regular_Algebras/document
20:16:56 Presenting document Regular_Algebras/outline
20:16:56 Presenting theory Regular_Algebras.Dioid_Power_Sum
20:16:56 Presenting theory Regular_Algebras.Regular_Algebras
20:16:56 Presenting theory Regular_Algebras.Regular_Algebra_Models
20:16:56 Presenting theory Regular_Algebras.Pratts_Counterexamples
20:16:56 Presenting theory Regular_Algebras.Regular_Algebra_Variants
20:16:56 Presenting Relation_Algebra ...
20:16:56 Presenting document Relation_Algebra/document
20:16:56 Presenting document Relation_Algebra/outline
20:16:56 Presenting theory Relation_Algebra.More_Boolean_Algebra
20:16:56 Presenting theory Relation_Algebra.Relation_Algebra
20:16:56 Presenting theory Relation_Algebra.Relation_Algebra_Vectors
20:16:56 Presenting theory Relation_Algebra.Relation_Algebra_Tests
20:16:56 Presenting theory Relation_Algebra.Relation_Algebra_Functions
20:16:56 Presenting theory Relation_Algebra.Relation_Algebra_Direct_Products
20:16:56 Presenting theory Relation_Algebra.Relation_Algebra_RTC
20:16:56 Presenting theory Relation_Algebra.Relation_Algebra_Models
20:16:56 Presenting Relational_Paths ...
20:16:56 Presenting document Relational_Paths/document
20:16:56 Presenting document Relational_Paths/outline
20:16:56 Presenting theory Relational_Paths.More_Relation_Algebra
20:16:56 Presenting theory Relational_Paths.Paths
20:16:56 Presenting theory Relational_Paths.Rooted_Paths
20:16:56 Presenting theory Relational_Paths.Path_Algorithms
20:16:57 Presenting Residuated_Lattices ...
20:16:57 Presenting document Residuated_Lattices/document
20:16:57 Presenting document Residuated_Lattices/outline
20:16:57 Presenting theory Residuated_Lattices.Residuated_Lattices
20:16:57 Presenting theory Residuated_Lattices.Residuated_Boolean_Algebras
20:16:57 Presenting theory Residuated_Lattices.Involutive_Residuated
20:16:57 Presenting theory Residuated_Lattices.Action_Algebra
20:16:57 Presenting theory Residuated_Lattices.Action_Algebra_Models
20:16:57 Presenting theory Residuated_Lattices.Residuated_Relation_Algebra
20:16:57 Presenting LEM ...
20:16:57 Presenting theory LEM.Lem_bool
20:16:57 Presenting theory LEM.Lem_basic_classes
20:16:57 Presenting theory LEM.Lem_tuple
20:16:57 Presenting theory LEM.Lem_function
20:16:57 Presenting theory LEM.Lem_maybe
20:16:57 Presenting theory LEM.Lem_num
20:16:57 Presenting theory LEM.LemExtraDefs
20:16:57 Presenting theory LEM.Lem
20:16:57 Presenting theory LEM.Lem_list
20:16:57 Presenting theory LEM.Lem_either
20:16:57 Presenting theory LEM.Lem_set_helpers
20:16:57 Presenting theory LEM.Lem_set
20:16:57 Presenting theory LEM.Lem_map
20:16:57 Presenting theory LEM.Lem_string
20:16:57 Presenting theory LEM.Lem_word
20:16:57 Presenting theory LEM.Lem_show
20:16:57 Presenting theory LEM.Lem_sorting
20:16:57 Presenting theory LEM.Lem_relation
20:16:57 Presenting theory LEM.Lem_pervasives
20:16:57 Presenting theory LEM.Lem_function_extra
20:16:57 Presenting theory LEM.Lem_assert_extra
20:16:57 Presenting theory LEM.Lem_maybe_extra
20:16:57 Presenting theory LEM.Lem_map_extra
20:16:57 Presenting theory LEM.Lem_num_extra
20:16:57 Presenting theory LEM.Lem_set_extra
20:16:57 Presenting theory LEM.Lem_list_extra
20:16:57 Presenting theory LEM.Lem_string_extra
20:16:57 Presenting theory LEM.Lem_show_extra
20:16:57 Presenting theory LEM.Lem_machine_word
20:16:57 Presenting theory LEM.Lem_pervasives_extra
20:16:57 Presenting CakeML ...
20:16:57 Presenting document CakeML/document
20:16:57 Presenting document CakeML/outline
20:16:57 Presenting theory CakeML.Doc_Generated
20:16:57 Presenting theory CakeML.Lib
20:16:57 Presenting theory CakeML.Namespace
20:16:57 Presenting theory CakeML.FpSem
20:16:57 Presenting theory CakeML.Ast
20:16:57 Presenting theory CakeML.AstAuxiliary
20:16:57 Presenting theory CakeML.Ffi
20:16:57 Presenting theory CakeML.SemanticPrimitives
20:16:57 Presenting theory CakeML.SmallStep
20:16:57 Presenting theory CakeML.BigStep
20:16:57 Presenting theory CakeML.BigSmallInvariants
20:16:57 Presenting theory CakeML.Evaluate
20:16:57 Presenting theory CakeML.LibAuxiliary
20:16:57 Presenting theory CakeML.NamespaceAuxiliary
20:16:57 Presenting theory CakeML.PrimTypes
20:16:57 Presenting theory CakeML.SemanticPrimitivesAuxiliary
20:16:57 Presenting theory CakeML.SimpleIO
20:16:58 Presenting theory CakeML.Tokens
20:16:58 Presenting theory CakeML.TypeSystem
20:16:58 Presenting theory CakeML.TypeSystemAuxiliary
20:16:58 Presenting theory CakeML.Doc_Proofs
20:16:58 Presenting theory CakeML.Semantic_Extras
20:16:58 Presenting theory CakeML.Evaluate_Termination
20:16:58 Presenting theory CakeML.Evaluate_Clock
20:16:58 Presenting theory CakeML.Evaluate_Single
20:16:58 Presenting theory CakeML.Big_Step_Determ
20:16:58 Presenting theory CakeML.Big_Step_Total
20:16:58 Presenting theory CakeML.Big_Step_Fun_Equiv
20:16:58 Presenting theory CakeML.Big_Step_Unclocked
20:16:58 Presenting theory CakeML.Big_Step_Clocked
20:16:58 Presenting theory CakeML.Big_Step_Unclocked_Single
20:16:58 Presenting theory CakeML.Matching
20:16:58 Presenting theory CakeML.CakeML_Code
20:16:58 Presenting theory CakeML.CakeML_Quickcheck
20:16:58 Presenting theory CakeML.CakeML_Compiler
20:16:58 Presenting theory CakeML.Compiler_Test
20:16:58 Presenting theory CakeML.Code_Test_Haskell
20:16:59 Presenting file "Tools/cakeml_sexp.ML"
20:16:59 Presenting file "Tools/cakeml_compiler.ML"
20:16:59 Presenting CakeML_Codegen ...
20:16:59 Presenting document CakeML_Codegen/document
20:16:59 Presenting document CakeML_Codegen/outline
20:16:59 Presenting theory CakeML_Codegen.ML_Utils
20:16:59 Presenting theory CakeML_Codegen.Compiler_Utils
20:16:59 Presenting theory CakeML_Codegen.Code_Utils
20:16:59 Presenting theory CakeML_Codegen.CakeML_Utils
20:16:59 Presenting theory CakeML_Codegen.Test_Utils
20:16:59 Presenting theory CakeML_Codegen.Doc_Terms
20:16:59 Presenting theory CakeML_Codegen.Terms_Extras
20:16:59 Presenting theory CakeML_Codegen.HOL_Datatype
20:16:59 Presenting theory CakeML_Codegen.Constructors
20:16:59 Presenting theory CakeML_Codegen.Consts
20:16:59 Presenting theory CakeML_Codegen.Strong_Term
20:16:59 Presenting theory CakeML_Codegen.Sterm
20:16:59 Presenting theory CakeML_Codegen.Pterm
20:16:59 Presenting file "hol_datatype.ML"
20:16:59 Presenting theory CakeML_Codegen.Term_as_Value
20:16:59 Presenting file "utils.ML"
20:16:59 Presenting theory CakeML_Codegen.Value
20:16:59 Presenting theory CakeML_Codegen.Doc_CupCake
20:16:59 Presenting theory CakeML_Codegen.CupCake_Env
20:16:59 Presenting theory CakeML_Codegen.CupCake_Semantics
20:16:59 Presenting file "pattern_compatibility.ML"
20:16:59 Presenting file "dynamic_unfold.ML"
20:16:59 Presenting theory CakeML_Codegen.Doc_Rewriting
20:16:59 Presenting theory CakeML_Codegen.General_Rewriting
20:16:59 Presenting theory CakeML_Codegen.Rewriting_Term
20:16:59 Presenting theory CakeML_Codegen.Rewriting_Nterm
20:16:59 Presenting file "hol_term.ML"
20:16:59 Presenting theory CakeML_Codegen.Rewriting_Pterm_Elim
20:16:59 Presenting theory CakeML_Codegen.Rewriting_Pterm
20:17:00 Presenting theory CakeML_Codegen.Rewriting_Sterm
20:17:00 Presenting theory CakeML_Codegen.Big_Step_Sterm
20:17:00 Presenting theory CakeML_Codegen.Big_Step_Value
20:17:00 Presenting theory CakeML_Codegen.Big_Step_Value_ML
20:17:00 Presenting theory CakeML_Codegen.Doc_Preproc
20:17:00 Presenting theory CakeML_Codegen.Eval_Class
20:17:00 Presenting theory CakeML_Codegen.Embed
20:17:00 Presenting theory CakeML_Codegen.Eval_Instances
20:17:00 Presenting theory CakeML_Codegen.Doc_Backend
20:17:00 Presenting theory CakeML_Codegen.CakeML_Setup
20:17:00 Presenting file "tactics.ML"
20:17:00 Presenting theory CakeML_Codegen.CakeML_Backend
20:17:00 Presenting theory CakeML_Codegen.CakeML_Correctness
20:17:00 Presenting file "eval_instances.ML"
20:17:00 Presenting theory CakeML_Codegen.CakeML_Byte
20:17:00 Presenting theory CakeML_Codegen.Doc_Compiler
20:17:00 Presenting theory CakeML_Codegen.Composition
20:17:01 Presenting theory CakeML_Codegen.Compiler
20:17:01 Presenting theory CakeML_Codegen.Test_Composition
20:17:01 Presenting theory CakeML_Codegen.Test_Print
20:17:01 Presenting file "embed.ML"
20:17:01 Presenting theory CakeML_Codegen.Test_Embed_Data
20:17:01 Presenting theory CakeML_Codegen.Test_Embed_Data2
20:17:01 Presenting theory CakeML_Codegen.Test_Embed_Tree
20:17:01 Presenting theory CakeML_Codegen.Test_Datatypes
20:17:02 Presenting LambdaMu ...
20:17:02 Presenting document LambdaMu/document
20:17:02 Presenting document LambdaMu/outline
20:17:02 Presenting theory LambdaMu.Syntax
20:17:02 Presenting theory LambdaMu.Types
20:17:02 Presenting theory LambdaMu.DeBruijn
20:17:02 Presenting theory LambdaMu.Substitution
20:17:02 Presenting theory LambdaMu.Reduction
20:17:02 Presenting theory LambdaMu.ContextFacts
20:17:02 Presenting theory LambdaMu.TypePreservation
20:17:02 Presenting theory LambdaMu.Progress
20:17:02 Presenting theory LambdaMu.Peirce
20:17:02 Presenting Latin_Square ...
20:17:02 Presenting document Latin_Square/document
20:17:02 Presenting document Latin_Square/outline
20:17:02 Presenting theory Latin_Square.Latin_Square
20:17:02 Presenting LatticeProperties ...
20:17:02 Presenting document LatticeProperties/document
20:17:02 Presenting document LatticeProperties/outline
20:17:02 Presenting theory LatticeProperties.WellFoundedTransitive
20:17:02 Presenting theory LatticeProperties.Complete_Lattice_Prop
20:17:02 Presenting theory LatticeProperties.Conj_Disj
20:17:02 Presenting theory LatticeProperties.Lattice_Prop
20:17:02 Presenting theory LatticeProperties.Modular_Distrib_Lattice
20:17:02 Presenting theory LatticeProperties.Lattice_Ordered_Group
20:17:02 Presenting Lazy_Case ...
20:17:02 Presenting document Lazy_Case/document
20:17:02 Presenting document Lazy_Case/outline
20:17:02 Presenting theory Lazy_Case.Lazy_Case
20:17:02 Presenting theory Lazy_Case.Test_Lazy_Case
20:17:02 Presenting file "lazy_case.ML"
20:17:02 Presenting Lifting_Definition_Option ...
20:17:02 Presenting document Lifting_Definition_Option/document
20:17:02 Presenting document Lifting_Definition_Option/outline
20:17:02 Presenting theory Lifting_Definition_Option.Lifting_Definition_Option_Examples
20:17:02 Presenting List-Index ...
20:17:02 Presenting document List-Index/document
20:17:02 Presenting document List-Index/outline
20:17:02 Presenting theory List-Index.List_Index
20:17:02 Presenting List_Interleaving ...
20:17:02 Presenting document List_Interleaving/document
20:17:02 Presenting document List_Interleaving/outline
20:17:02 Presenting theory List_Interleaving.ListInterleaving
20:17:03 Presenting List_Inversions ...
20:17:03 Presenting document List_Inversions/document
20:17:03 Presenting document List_Inversions/outline
20:17:03 Presenting theory List_Inversions.List_Inversions
20:17:03 Presenting LocalLexing ...
20:17:03 Presenting document LocalLexing/document
20:17:03 Presenting document LocalLexing/outline
20:17:03 Presenting theory LocalLexing.CFG
20:17:03 Presenting theory LocalLexing.LocalLexing
20:17:03 Presenting theory LocalLexing.LLEarleyParsing
20:17:03 Presenting theory LocalLexing.Limit
20:17:03 Presenting theory LocalLexing.LocalLexingLemmas
20:17:03 Presenting theory LocalLexing.InductRules
20:17:03 Presenting theory LocalLexing.ListTools
20:17:03 Presenting theory LocalLexing.Derivations
20:17:03 Presenting theory LocalLexing.Validity
20:17:03 Presenting theory LocalLexing.TheoremD2
20:17:03 Presenting theory LocalLexing.TheoremD4
20:17:03 Presenting theory LocalLexing.TheoremD5
20:17:03 Presenting theory LocalLexing.TheoremD6
20:17:03 Presenting theory LocalLexing.TheoremD7
20:17:03 Presenting theory LocalLexing.TheoremD8
20:17:03 Presenting theory LocalLexing.TheoremD9
20:17:03 Presenting theory LocalLexing.Ladder
20:17:03 Presenting theory LocalLexing.TheoremD10
20:17:04 Presenting theory LocalLexing.TheoremD11
20:17:04 Presenting theory LocalLexing.TheoremD12
20:17:04 Presenting theory LocalLexing.TheoremD13
20:17:04 Presenting theory LocalLexing.TheoremD14
20:17:04 Presenting theory LocalLexing.PathLemmas
20:17:04 Presenting theory LocalLexing.MainTheorems
20:17:05 Presenting Locally-Nameless-Sigma ...
20:17:05 Presenting document Locally-Nameless-Sigma/document
20:17:05 Presenting document Locally-Nameless-Sigma/outline
20:17:05 Presenting theory Locally-Nameless-Sigma.ListPre
20:17:05 Presenting theory Locally-Nameless-Sigma.FMap
20:17:05 Presenting theory Locally-Nameless-Sigma.Sigma
20:17:05 Presenting theory Locally-Nameless-Sigma.ParRed
20:17:05 Presenting theory Locally-Nameless-Sigma.Environments
20:17:05 Presenting theory Locally-Nameless-Sigma.TypedSigma
20:17:05 Presenting theory Locally-Nameless-Sigma.Locally_Nameless_Sigma
20:17:07 Presenting Logging_Independent_Anonymity ...
20:17:07 Presenting document Logging_Independent_Anonymity/document
20:17:07 Presenting document Logging_Independent_Anonymity/outline
20:17:07 Presenting theory Logging_Independent_Anonymity.Definitions
20:17:07 Presenting theory Logging_Independent_Anonymity.Anonymity
20:17:07 Presenting theory Logging_Independent_Anonymity.Possibility
20:17:07 Presenting Lowe_Ontological_Argument ...
20:17:07 Presenting document Lowe_Ontological_Argument/document
20:17:07 Presenting document Lowe_Ontological_Argument/outline
20:17:07 Presenting theory Lowe_Ontological_Argument.Relations
20:17:07 Presenting theory Lowe_Ontological_Argument.QML
20:17:07 Presenting theory Lowe_Ontological_Argument.LoweOntologicalArgument_1
20:17:07 Presenting theory Lowe_Ontological_Argument.LoweOntologicalArgument_2
20:17:07 Presenting theory Lowe_Ontological_Argument.LoweOntologicalArgument_3
20:17:07 Presenting theory Lowe_Ontological_Argument.LoweOntologicalArgument_4
20:17:07 Presenting theory Lowe_Ontological_Argument.LoweOntologicalArgument_5
20:17:07 Presenting theory Lowe_Ontological_Argument.LoweOntologicalArgument_6
20:17:07 Presenting theory Lowe_Ontological_Argument.LoweOntologicalArgument_7
20:17:07 Presenting MSO_Regex_Equivalence ...
20:17:07 Presenting document MSO_Regex_Equivalence/document
20:17:07 Presenting document MSO_Regex_Equivalence/outline
20:17:07 Presenting theory MSO_Regex_Equivalence.List_More
20:17:07 Presenting theory MSO_Regex_Equivalence.Pi_Regular_Set
20:17:07 Presenting theory MSO_Regex_Equivalence.Pi_Regular_Exp
20:17:07 Presenting theory MSO_Regex_Equivalence.Pi_Derivatives
20:17:07 Presenting theory MSO_Regex_Equivalence.Pi_Regular_Operators
20:17:07 Presenting theory MSO_Regex_Equivalence.Pi_Regular_Exp_Dual
20:17:07 Presenting theory MSO_Regex_Equivalence.Pi_Equivalence_Checking
20:17:07 Presenting theory MSO_Regex_Equivalence.Init_Normalization
20:17:07 Presenting theory MSO_Regex_Equivalence.PNormalization
20:17:07 Presenting theory MSO_Regex_Equivalence.Formula
20:17:07 Presenting theory MSO_Regex_Equivalence.M2L
20:17:07 Presenting theory MSO_Regex_Equivalence.M2L_Normalization
20:17:07 Presenting theory MSO_Regex_Equivalence.M2L_Equivalence_Checking
20:17:07 Presenting theory MSO_Regex_Equivalence.WS1S
20:17:07 Presenting theory MSO_Regex_Equivalence.WS1S_Normalization
20:17:07 Presenting theory MSO_Regex_Equivalence.WS1S_Equivalence_Checking
20:17:07 Presenting theory MSO_Regex_Equivalence.M2L_Examples
20:17:07 Presenting theory MSO_Regex_Equivalence.WS1S_Examples
20:17:08 Presenting Marriage ...
20:17:08 Presenting document Marriage/document
20:17:08 Presenting document Marriage/outline
20:17:08 Presenting theory Marriage.Marriage
20:17:09 Presenting Matroids ...
20:17:09 Presenting document Matroids/document
20:17:09 Presenting document Matroids/outline
20:17:09 Presenting theory Matroids.Indep_System
20:17:09 Presenting theory Matroids.Matroid
20:17:09 Presenting Max-Card-Matching ...
20:17:09 Presenting document Max-Card-Matching/document
20:17:09 Presenting document Max-Card-Matching/outline
20:17:09 Presenting theory Max-Card-Matching.Matching
20:17:09 Presenting Median_Of_Medians_Selection ...
20:17:09 Presenting document Median_Of_Medians_Selection/document
20:17:09 Presenting document Median_Of_Medians_Selection/outline
20:17:09 Presenting theory Median_Of_Medians_Selection.Median_Of_Medians_Selection
20:17:09 Presenting Menger ...
20:17:09 Presenting document Menger/document
20:17:09 Presenting document Menger/outline
20:17:09 Presenting theory Menger.Helpers
20:17:09 Presenting theory Menger.Graph
20:17:09 Presenting theory Menger.Separations
20:17:09 Presenting theory Menger.DisjointPaths
20:17:09 Presenting theory Menger.MengerInduction
20:17:09 Presenting theory Menger.Y_eq_new_last
20:17:09 Presenting theory Menger.Y_neq_new_last
20:17:09 Presenting theory Menger.Menger
20:17:09 Presenting Mereology ...
20:17:09 Presenting document Mereology/document
20:17:09 Presenting document Mereology/outline
20:17:09 Presenting theory Mereology.PM
20:17:09 Presenting theory Mereology.M
20:17:09 Presenting theory Mereology.MM
20:17:09 Presenting theory Mereology.EM
20:17:09 Presenting theory Mereology.CM
20:17:09 Presenting theory Mereology.CEM
20:17:09 Presenting theory Mereology.GM
20:17:09 Presenting theory Mereology.GMM
20:17:09 Presenting theory Mereology.GEM
20:17:10 Presenting Metalogic_ProofChecker ...
20:17:10 Presenting document Metalogic_ProofChecker/document
20:17:10 Presenting document Metalogic_ProofChecker/outline
20:17:10 Presenting theory Metalogic_ProofChecker.Core
20:17:10 Presenting theory Metalogic_ProofChecker.Preliminaries
20:17:10 Presenting theory Metalogic_ProofChecker.Term
20:17:10 Presenting theory Metalogic_ProofChecker.Sorts
20:17:10 Presenting theory Metalogic_ProofChecker.SortConstants
20:17:10 Presenting theory Metalogic_ProofChecker.Theory
20:17:10 Presenting theory Metalogic_ProofChecker.Term_Subst
20:17:10 Presenting theory Metalogic_ProofChecker.Name
20:17:10 Presenting theory Metalogic_ProofChecker.BetaNorm
20:17:10 Presenting theory Metalogic_ProofChecker.BetaNormProof
20:17:10 Presenting theory Metalogic_ProofChecker.EtaNorm
20:17:10 Presenting theory Metalogic_ProofChecker.EtaNormProof
20:17:10 Presenting theory Metalogic_ProofChecker.Logic
20:17:10 Presenting theory Metalogic_ProofChecker.EqualityProof
20:17:10 Presenting theory Metalogic_ProofChecker.ProofTerm
20:17:10 Presenting theory Metalogic_ProofChecker.SortsExe
20:17:10 Presenting theory Metalogic_ProofChecker.Instances
20:17:11 Presenting theory Metalogic_ProofChecker.TheoryExe
20:17:11 Presenting theory Metalogic_ProofChecker.CheckerExe
20:17:11 Presenting theory Metalogic_ProofChecker.CodeGen
20:17:12 Presenting MiniML ...
20:17:12 Presenting document MiniML/document
20:17:12 Presenting document MiniML/outline
20:17:12 Presenting theory MiniML.Maybe
20:17:12 Presenting theory MiniML.Type
20:17:12 Presenting theory MiniML.Instance
20:17:12 Presenting theory MiniML.Generalize
20:17:12 Presenting theory MiniML.MiniML
20:17:12 Presenting theory MiniML.W
20:17:13 Presenting Modular_Assembly_Kit_Security ...
20:17:13 Presenting document Modular_Assembly_Kit_Security/document
20:17:13 Presenting document Modular_Assembly_Kit_Security/outline
20:17:13 Presenting theory Modular_Assembly_Kit_Security.Projection
20:17:13 Presenting theory Modular_Assembly_Kit_Security.Prefix
20:17:13 Presenting theory Modular_Assembly_Kit_Security.EventSystems
20:17:13 Presenting theory Modular_Assembly_Kit_Security.StateEventSystems
20:17:13 Presenting theory Modular_Assembly_Kit_Security.Views
20:17:13 Presenting theory Modular_Assembly_Kit_Security.FlowPolicies
20:17:13 Presenting theory Modular_Assembly_Kit_Security.BasicSecurityPredicates
20:17:13 Presenting theory Modular_Assembly_Kit_Security.InformationFlowProperties
20:17:13 Presenting theory Modular_Assembly_Kit_Security.BSPTaxonomy
20:17:13 Presenting theory Modular_Assembly_Kit_Security.PropertyLibrary
20:17:13 Presenting theory Modular_Assembly_Kit_Security.SecureSystems
20:17:13 Presenting theory Modular_Assembly_Kit_Security.UnwindingConditions
20:17:13 Presenting theory Modular_Assembly_Kit_Security.AuxiliaryLemmas
20:17:13 Presenting theory Modular_Assembly_Kit_Security.UnwindingResults
20:17:13 Presenting theory Modular_Assembly_Kit_Security.CompositionBase
20:17:13 Presenting theory Modular_Assembly_Kit_Security.CompositionSupport
20:17:13 Presenting theory Modular_Assembly_Kit_Security.GeneralizedZippingLemma
20:17:13 Presenting theory Modular_Assembly_Kit_Security.CompositionalityResults
20:17:14 Presenting Monad_Memo_DP ...
20:17:14 Presenting document Monad_Memo_DP/document
20:17:14 Presenting document Monad_Memo_DP/outline
20:17:14 Presenting theory Monad_Memo_DP.State_Monad_Ext
20:17:14 Presenting theory Monad_Memo_DP.Pure_Monad
20:17:14 Presenting theory Monad_Memo_DP.DP_CRelVS
20:17:14 Presenting theory Monad_Memo_DP.State_Heap_Misc
20:17:14 Presenting theory Monad_Memo_DP.Heap_Monad_Ext
20:17:14 Presenting theory Monad_Memo_DP.State_Heap
20:17:14 Presenting theory Monad_Memo_DP.DP_CRelVH
20:17:14 Presenting theory Monad_Memo_DP.Memory
20:17:14 Presenting theory Monad_Memo_DP.Pair_Memory
20:17:14 Presenting theory Monad_Memo_DP.Index
20:17:14 Presenting theory Monad_Memo_DP.Memory_Heap
20:17:14 Presenting theory Monad_Memo_DP.Transform_Cmd
20:17:14 Presenting theory Monad_Memo_DP.Bottom_Up_Computation
20:17:14 Presenting theory Monad_Memo_DP.Bottom_Up_Computation_Heap
20:17:14 Presenting theory Monad_Memo_DP.Solve_Cong
20:17:14 Presenting theory Monad_Memo_DP.Heap_Main
20:17:14 Presenting theory Monad_Memo_DP.State_Main
20:17:14 Presenting theory Monad_Memo_DP.Example_Misc
20:17:14 Presenting theory Monad_Memo_DP.Tracing
20:17:14 Presenting theory Monad_Memo_DP.Ground_Function
20:17:14 Presenting theory Monad_Memo_DP.Bellman_Ford
20:17:14 Presenting theory Monad_Memo_DP.Heap_Default
20:17:14 Presenting file "Ground_Function.ML"
20:17:14 Presenting theory Monad_Memo_DP.Knapsack
20:17:14 Presenting theory Monad_Memo_DP.Counting_Tiles
20:17:14 Presenting theory Monad_Memo_DP.CYK
20:17:14 Presenting theory Monad_Memo_DP.Min_Ed_Dist0
20:17:14 Presenting theory Monad_Memo_DP.OptBST
20:17:15 Presenting theory Monad_Memo_DP.Longest_Common_Subsequence
20:17:15 Presenting theory Monad_Memo_DP.All_Examples
20:17:15 Presenting file "Transform_Misc.ML"
20:17:15 Presenting file "Transform_Const.ML"
20:17:15 Presenting file "Transform_Data.ML"
20:17:15 Presenting file "Transform_Tactic.ML"
20:17:15 Presenting file "Transform_Term.ML"
20:17:15 Presenting file "Transform.ML"
20:17:15 Presenting file "Transform_Parser.ML"
20:17:15 Presenting Optimal_BST ...
20:17:15 Presenting document Optimal_BST/document
20:17:15 Presenting document Optimal_BST/outline
20:17:15 Presenting theory Optimal_BST.Weighted_Path_Length
20:17:15 Presenting theory Optimal_BST.Optimal_BST
20:17:15 Presenting theory Optimal_BST.Quadrilateral_Inequality
20:17:15 Presenting theory Optimal_BST.Optimal_BST2
20:17:15 Presenting theory Optimal_BST.Optimal_BST_Examples
20:17:15 Presenting theory Optimal_BST.Optimal_BST_Code
20:17:15 Presenting theory Optimal_BST.Optimal_BST_Memo
20:17:15 Presenting MonoBoolTranAlgebra ...
20:17:15 Presenting document MonoBoolTranAlgebra/document
20:17:15 Presenting document MonoBoolTranAlgebra/outline
20:17:15 Presenting theory MonoBoolTranAlgebra.Mono_Bool_Tran
20:17:15 Presenting theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra
20:17:15 Presenting theory MonoBoolTranAlgebra.Assertion_Algebra
20:17:15 Presenting theory MonoBoolTranAlgebra.Statements
20:17:16 Presenting Name_Carrying_Type_Inference ...
20:17:16 Presenting document Name_Carrying_Type_Inference/document
20:17:16 Presenting document Name_Carrying_Type_Inference/outline
20:17:16 Presenting theory Name_Carrying_Type_Inference.Fresh
20:17:16 Presenting theory Name_Carrying_Type_Inference.Permutation
20:17:16 Presenting theory Name_Carrying_Type_Inference.PreSimplyTyped
20:17:16 Presenting theory Name_Carrying_Type_Inference.SimplyTyped
20:17:16 Presenting Nash_Williams ...
20:17:16 Presenting document Nash_Williams/document
20:17:16 Presenting document Nash_Williams/outline
20:17:16 Presenting theory Nash_Williams.Nash_Extras
20:17:16 Presenting theory Nash_Williams.Nash_Williams
20:17:17 Presenting Network_Security_Policy_Verification ...
20:17:17 Presenting document Network_Security_Policy_Verification/document
20:17:17 Presenting document Network_Security_Policy_Verification/outline
20:17:17 Presenting theory Network_Security_Policy_Verification.ML_GraphViz
20:17:17 Presenting theory Network_Security_Policy_Verification.ML_GraphViz_Disable
20:17:17 Presenting theory Network_Security_Policy_Verification.FiniteGraph
20:17:17 Presenting theory Network_Security_Policy_Verification.FiniteListGraph
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Util
20:17:17 Presenting theory Network_Security_Policy_Verification.Efficient_Distinct
20:17:17 Presenting theory Network_Security_Policy_Verification.FiniteListGraph_Impl
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Vertices
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Interface
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_withOffendingFlows
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_ENF
20:17:17 Presenting theory Network_Security_Policy_Verification.vertex_example_simps
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Helper
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Subnets2
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_BLPstrict
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Tainting
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_BLPbasic
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_BLPtrusted
20:17:17 Presenting theory Network_Security_Policy_Verification.Analysis_Tainting
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Interface_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_BLPbasic_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Subnets
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Subnets_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_BLPtrusted_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_SecGwExt
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_SecGwExt_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Sink
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Sink_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_NoRefl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_NoRefl_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Tainting_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Dependability
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Dependability_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_NonInterference
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_NonInterference_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl
20:17:17 Presenting theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Library
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Composition_Theory
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Stateful_Policy
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Composition_Theory_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_Algorithm
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_impl
20:17:17 Presenting theory Network_Security_Policy_Verification.METASINVAR_SystemBoundary
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_Impl
20:17:17 Presenting theory Network_Security_Policy_Verification.Network_Security_Policy_Verification
20:17:17 Presenting theory Network_Security_Policy_Verification.Example_BLP
20:17:17 Presenting theory Network_Security_Policy_Verification.TopoS_generateCode
20:17:18 Presenting theory Network_Security_Policy_Verification.attic
20:17:18 Presenting theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork
20:17:18 Presenting theory Network_Security_Policy_Verification.Impl_List_Playground_statefulpolicycompliance
20:17:18 Presenting theory Network_Security_Policy_Verification.Example
20:17:18 Presenting theory Network_Security_Policy_Verification.Example_NetModel
20:17:18 Presenting theory Network_Security_Policy_Verification.Example_Forte14
20:17:18 Presenting theory Network_Security_Policy_Verification.Distributed_WebApp
20:17:18 Presenting theory Network_Security_Policy_Verification.I8_SSH_Landscape
20:17:18 Presenting theory Network_Security_Policy_Verification.Impl_List_Playground
20:17:18 Presenting theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork_statefulpolicy_example
20:17:18 Presenting theory Network_Security_Policy_Verification.CryptoDB
20:17:18 Presenting theory Network_Security_Policy_Verification.IDEM
20:17:18 Presenting theory Network_Security_Policy_Verification.MeasrDroid
20:17:18 Presenting theory Network_Security_Policy_Verification.SINVAR_Examples
20:17:18 Presenting theory Network_Security_Policy_Verification.Imaginary_Factory_Network
20:17:20 Presenting No_FTL_observers ...
20:17:20 Presenting document No_FTL_observers/document
20:17:20 Presenting document No_FTL_observers/outline
20:17:20 Presenting theory No_FTL_observers.SpaceTime
20:17:20 Presenting theory No_FTL_observers.SomeFunc
20:17:20 Presenting theory No_FTL_observers.Axioms
20:17:20 Presenting theory No_FTL_observers.SpecRel
20:17:20 Presenting Nominal2 ...
20:17:20 Presenting document Nominal2/document
20:17:20 Presenting document Nominal2/outline
20:17:20 Presenting theory Nominal2.Nominal2_Base
20:17:20 Presenting theory Nominal2.Nominal2_Abs
20:17:20 Presenting theory Nominal2.Nominal2_FCB
20:17:20 Presenting theory Nominal2.Nominal2
20:17:20 Presenting theory Nominal2.Atoms
20:17:20 Presenting theory Nominal2.Eqvt
20:17:21 Presenting file "nominal_basics.ML"
20:17:21 Presenting file "nominal_thmdecls.ML"
20:17:21 Presenting file "nominal_permeq.ML"
20:17:21 Presenting file "nominal_library.ML"
20:17:21 Presenting file "nominal_atoms.ML"
20:17:21 Presenting file "nominal_eqvt.ML"
20:17:22 Presenting file "nominal_dt_data.ML"
20:17:22 Presenting file "nominal_dt_rawfuns.ML"
20:17:22 Presenting file "nominal_dt_alpha.ML"
20:17:22 Presenting file "nominal_dt_quot.ML"
20:17:22 Presenting file "nominal_induct.ML"
20:17:22 Presenting file "nominal_inductive.ML"
20:17:22 Presenting file "nominal_function_common.ML"
20:17:22 Presenting file "nominal_function_core.ML"
20:17:22 Presenting file "nominal_mutual.ML"
20:17:22 Presenting file "nominal_function.ML"
20:17:22 Presenting file "nominal_termination.ML"
20:17:22 Presenting LambdaAuth ...
20:17:22 Presenting document LambdaAuth/document
20:17:22 Presenting document LambdaAuth/outline
20:17:22 Presenting theory LambdaAuth.Nominal2_Lemmas
20:17:22 Presenting theory LambdaAuth.FMap_Lemmas
20:17:22 Presenting theory LambdaAuth.Syntax
20:17:22 Presenting theory LambdaAuth.Semantics
20:17:22 Presenting theory LambdaAuth.Agreement
20:17:22 Presenting theory LambdaAuth.Results
20:17:22 Presenting Modal_Logics_for_NTS ...
20:17:22 Presenting document Modal_Logics_for_NTS/document
20:17:22 Presenting document Modal_Logics_for_NTS/outline
20:17:22 Presenting theory Modal_Logics_for_NTS.Nominal_Bounded_Set
20:17:22 Presenting theory Modal_Logics_for_NTS.Nominal_Wellfounded
20:17:22 Presenting theory Modal_Logics_for_NTS.Residual
20:17:22 Presenting theory Modal_Logics_for_NTS.Transition_System
20:17:22 Presenting theory Modal_Logics_for_NTS.Formula
20:17:22 Presenting theory Modal_Logics_for_NTS.Validity
20:17:22 Presenting theory Modal_Logics_for_NTS.Logical_Equivalence
20:17:22 Presenting theory Modal_Logics_for_NTS.Bisimilarity_Implies_Equivalence
20:17:22 Presenting theory Modal_Logics_for_NTS.Equivalence_Implies_Bisimilarity
20:17:22 Presenting theory Modal_Logics_for_NTS.Disjunction
20:17:22 Presenting theory Modal_Logics_for_NTS.Expressive_Completeness
20:17:22 Presenting theory Modal_Logics_for_NTS.FS_Set
20:17:22 Presenting theory Modal_Logics_for_NTS.FL_Transition_System
20:17:22 Presenting theory Modal_Logics_for_NTS.FL_Formula
20:17:22 Presenting theory Modal_Logics_for_NTS.FL_Validity
20:17:23 Presenting theory Modal_Logics_for_NTS.FL_Logical_Equivalence
20:17:23 Presenting theory Modal_Logics_for_NTS.FL_Bisimilarity_Implies_Equivalence
20:17:23 Presenting theory Modal_Logics_for_NTS.FL_Equivalence_Implies_Bisimilarity
20:17:23 Presenting theory Modal_Logics_for_NTS.L_Transform
20:17:23 Presenting theory Modal_Logics_for_NTS.Weak_Transition_System
20:17:23 Presenting theory Modal_Logics_for_NTS.Weak_Formula
20:17:23 Presenting theory Modal_Logics_for_NTS.Weak_Validity
20:17:23 Presenting theory Modal_Logics_for_NTS.Weak_Logical_Equivalence
20:17:23 Presenting theory Modal_Logics_for_NTS.Weak_Bisimilarity_Implies_Equivalence
20:17:23 Presenting theory Modal_Logics_for_NTS.Weak_Equivalence_Implies_Bisimilarity
20:17:23 Presenting theory Modal_Logics_for_NTS.Weak_Expressive_Completeness
20:17:23 Presenting theory Modal_Logics_for_NTS.S_Transform
20:17:24 Presenting Rewriting_Z ...
20:17:24 Presenting document Rewriting_Z/document
20:17:24 Presenting document Rewriting_Z/outline
20:17:24 Presenting theory Rewriting_Z.Z
20:17:24 Presenting theory Rewriting_Z.Lambda_Z
20:17:24 Presenting theory Rewriting_Z.CL_Z
20:17:24 Presenting Noninterference_CSP ...
20:17:24 Presenting document Noninterference_CSP/document
20:17:24 Presenting document Noninterference_CSP/outline
20:17:24 Presenting theory Noninterference_CSP.CSPNoninterference
20:17:24 Presenting theory Noninterference_CSP.ClassicalNoninterference
20:17:24 Presenting theory Noninterference_CSP.GeneralizedNoninterference
20:17:25 Presenting Noninterference_Ipurge_Unwinding ...
20:17:25 Presenting document Noninterference_Ipurge_Unwinding/document
20:17:25 Presenting document Noninterference_Ipurge_Unwinding/outline
20:17:25 Presenting theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding
20:17:25 Presenting theory Noninterference_Ipurge_Unwinding.DeterministicProcesses
20:17:25 Presenting Noninterference_Generic_Unwinding ...
20:17:25 Presenting document Noninterference_Generic_Unwinding/document
20:17:25 Presenting document Noninterference_Generic_Unwinding/outline
20:17:25 Presenting theory Noninterference_Generic_Unwinding.GenericUnwinding
20:17:26 Presenting Noninterference_Inductive_Unwinding ...
20:17:26 Presenting document Noninterference_Inductive_Unwinding/document
20:17:26 Presenting document Noninterference_Inductive_Unwinding/outline
20:17:26 Presenting theory Noninterference_Inductive_Unwinding.InductiveUnwinding
20:17:26 Presenting Noninterference_Sequential_Composition ...
20:17:26 Presenting document Noninterference_Sequential_Composition/document
20:17:26 Presenting document Noninterference_Sequential_Composition/outline
20:17:26 Presenting theory Noninterference_Sequential_Composition.Propaedeutics
20:17:26 Presenting theory Noninterference_Sequential_Composition.SequentialComposition
20:17:26 Presenting theory Noninterference_Sequential_Composition.Counterexamples
20:17:27 Presenting Noninterference_Concurrent_Composition ...
20:17:27 Presenting document Noninterference_Concurrent_Composition/document
20:17:27 Presenting document Noninterference_Concurrent_Composition/outline
20:17:27 Presenting theory Noninterference_Concurrent_Composition.ConcurrentComposition
20:17:28 Presenting NormByEval ...
20:17:28 Presenting document NormByEval/document
20:17:28 Presenting document NormByEval/outline
20:17:28 Presenting theory NormByEval.NBE
20:17:28 Presenting OpSets ...
20:17:28 Presenting document OpSets/document
20:17:28 Presenting document OpSets/outline
20:17:28 Presenting theory OpSets.OpSet
20:17:28 Presenting theory OpSets.Insert_Spec
20:17:28 Presenting theory OpSets.List_Spec
20:17:28 Presenting theory OpSets.Interleaving
20:17:28 Presenting theory OpSets.RGA
20:17:29 Presenting Open_Induction ...
20:17:29 Presenting document Open_Induction/document
20:17:29 Presenting document Open_Induction/outline
20:17:29 Presenting theory Open_Induction.Restricted_Predicates
20:17:29 Presenting theory Open_Induction.Open_Induction
20:17:29 Presenting Ordinal ...
20:17:29 Presenting document Ordinal/document
20:17:29 Presenting document Ordinal/outline
20:17:29 Presenting theory Ordinal.OrdinalDef
20:17:29 Presenting theory Ordinal.OrdinalInduct
20:17:29 Presenting theory Ordinal.OrdinalCont
20:17:29 Presenting theory Ordinal.OrdinalRec
20:17:29 Presenting theory Ordinal.OrdinalArith
20:17:29 Presenting theory Ordinal.OrdinalInverse
20:17:29 Presenting theory Ordinal.OrdinalFix
20:17:29 Presenting theory Ordinal.OrdinalOmega
20:17:29 Presenting theory Ordinal.OrdinalVeblen
20:17:29 Presenting theory Ordinal.Ordinal
20:17:30 Presenting Nested_Multisets_Ordinals ...
20:17:30 Presenting document Nested_Multisets_Ordinals/document
20:17:30 Presenting document Nested_Multisets_Ordinals/outline
20:17:30 Presenting theory Nested_Multisets_Ordinals.Multiset_More
20:17:30 Presenting theory Nested_Multisets_Ordinals.Signed_Multiset
20:17:30 Presenting theory Nested_Multisets_Ordinals.Nested_Multiset
20:17:30 Presenting theory Nested_Multisets_Ordinals.Hereditary_Multiset
20:17:30 Presenting theory Nested_Multisets_Ordinals.Signed_Hereditary_Multiset
20:17:30 Presenting theory Nested_Multisets_Ordinals.Syntactic_Ordinal
20:17:30 Presenting theory Nested_Multisets_Ordinals.Signed_Syntactic_Ordinal
20:17:30 Presenting theory Nested_Multisets_Ordinals.Syntactic_Ordinal_Bridge
20:17:30 Presenting theory Nested_Multisets_Ordinals.McCarthy_91
20:17:30 Presenting theory Nested_Multisets_Ordinals.Hydra_Battle
20:17:30 Presenting theory Nested_Multisets_Ordinals.Goodstein_Sequence
20:17:30 Presenting theory Nested_Multisets_Ordinals.Unary_PCF
20:17:30 Presenting file "zmultiset_simprocs.ML"
20:17:30 Presenting Lambda_Free_KBOs ...
20:17:30 Presenting document Lambda_Free_KBOs/document
20:17:30 Presenting document Lambda_Free_KBOs/outline
20:17:30 Presenting theory Lambda_Free_KBOs.Lambda_Free_KBO_Util
20:17:30 Presenting theory Lambda_Free_KBOs.Lambda_Free_KBO_App
20:17:30 Presenting theory Lambda_Free_KBOs.Lambda_Free_KBO_Std
20:17:30 Presenting theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic
20:17:30 Presenting theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs
20:17:30 Presenting theory Lambda_Free_KBOs.Lambda_Encoding_KBO
20:17:30 Presenting theory Lambda_Free_KBOs.Lambda_Free_KBOs
20:17:31 Presenting Progress_Tracking ...
20:17:31 Presenting document Progress_Tracking/document
20:17:31 Presenting document Progress_Tracking/outline
20:17:31 Presenting theory Progress_Tracking.Auxiliary
20:17:31 Presenting theory Progress_Tracking.Exchange_Abadi
20:17:31 Presenting theory Progress_Tracking.Exchange
20:17:31 Presenting theory Progress_Tracking.Antichain
20:17:31 Presenting theory Progress_Tracking.Graph
20:17:31 Presenting theory Progress_Tracking.Propagate
20:17:31 Presenting theory Progress_Tracking.Combined
20:17:32 Presenting Ordinal_Partitions ...
20:17:32 Presenting document Ordinal_Partitions/document
20:17:32 Presenting document Ordinal_Partitions/outline
20:17:32 Presenting theory Ordinal_Partitions.Library_Additions
20:17:32 Presenting theory Ordinal_Partitions.Partitions
20:17:32 Presenting theory Ordinal_Partitions.Erdos_Milner
20:17:32 Presenting theory Ordinal_Partitions.Omega_Omega
20:17:33 Presenting PLM ...
20:17:33 Presenting document PLM/document
20:17:33 Presenting document PLM/outline
20:17:33 Presenting theory PLM.TAO_1_Embedding
20:17:33 Presenting theory PLM.TAO_2_Semantics
20:17:33 Presenting theory PLM.TAO_3_Quantifiable
20:17:33 Presenting theory PLM.TAO_4_BasicDefinitions
20:17:33 Presenting theory PLM.TAO_5_MetaSolver
20:17:33 Presenting theory PLM.TAO_6_Identifiable
20:17:33 Presenting theory PLM.TAO_7_Axioms
20:17:33 Presenting theory PLM.TAO_8_Definitions
20:17:33 Presenting theory PLM.TAO_9_PLM
20:17:33 Presenting theory PLM.TAO_10_PossibleWorlds
20:17:33 Presenting theory PLM.TAO_98_ArtificialTheorems
20:17:33 Presenting theory PLM.TAO_99_SanityTests
20:17:33 Presenting theory PLM.TAO_99_Paradox
20:17:33 Presenting theory PLM.Thesis
20:17:34 Presenting PSemigroupsConvolution ...
20:17:34 Presenting document PSemigroupsConvolution/document
20:17:34 Presenting document PSemigroupsConvolution/outline
20:17:34 Presenting theory PSemigroupsConvolution.Partial_Semigroups
20:17:34 Presenting theory PSemigroupsConvolution.Partial_Semigroup_Models
20:17:34 Presenting theory PSemigroupsConvolution.Quantales
20:17:34 Presenting theory PSemigroupsConvolution.Binary_Modalities
20:17:34 Presenting theory PSemigroupsConvolution.Unary_Modalities
20:17:34 Presenting theory PSemigroupsConvolution.Partial_Semigroup_Lifting
20:17:35 Presenting Paraconsistency ...
20:17:35 Presenting document Paraconsistency/document
20:17:35 Presenting document Paraconsistency/outline
20:17:35 Presenting theory Paraconsistency.Paraconsistency
20:17:35 Presenting Parity_Game ...
20:17:35 Presenting document Parity_Game/document
20:17:35 Presenting document Parity_Game/outline
20:17:35 Presenting theory Parity_Game.MoreCoinductiveList
20:17:35 Presenting theory Parity_Game.ParityGame
20:17:35 Presenting theory Parity_Game.Strategy
20:17:35 Presenting theory Parity_Game.AttractingStrategy
20:17:35 Presenting theory Parity_Game.Attractor
20:17:35 Presenting theory Parity_Game.WinningStrategy
20:17:35 Presenting theory Parity_Game.WellOrderedStrategy
20:17:35 Presenting theory Parity_Game.WinningRegion
20:17:35 Presenting theory Parity_Game.UniformStrategy
20:17:35 Presenting theory Parity_Game.AttractorStrategy
20:17:35 Presenting theory Parity_Game.PositionalDeterminacy
20:17:35 Presenting theory Parity_Game.AttractorInductive
20:17:35 Presenting theory Parity_Game.Graph_TheoryCompatibility
20:17:35 Presenting GaleStewart_Games ...
20:17:35 Presenting document GaleStewart_Games/document
20:17:35 Presenting document GaleStewart_Games/outline
20:17:35 Presenting theory GaleStewart_Games.MoreCoinductiveList2
20:17:35 Presenting theory GaleStewart_Games.MoreENat
20:17:35 Presenting theory GaleStewart_Games.MorePrefix
20:17:35 Presenting theory GaleStewart_Games.AlternatingLists
20:17:35 Presenting theory GaleStewart_Games.GaleStewartGames
20:17:35 Presenting theory GaleStewart_Games.GaleStewartDefensiveStrategies
20:17:35 Presenting theory GaleStewart_Games.GaleStewartDeterminedGames
20:17:36 Presenting Partial_Function_MR ...
20:17:36 Presenting document Partial_Function_MR/document
20:17:36 Presenting document Partial_Function_MR/outline
20:17:36 Presenting theory Partial_Function_MR.Partial_Function_MR
20:17:36 Presenting theory Partial_Function_MR.Partial_Function_MR_Examples
20:17:36 Presenting file "partial_function_mr.ML"
20:17:36 Presenting Physical_Quantities ...
20:17:36 Presenting document Physical_Quantities/document
20:17:36 Presenting document Physical_Quantities/outline
20:17:36 Presenting theory Physical_Quantities.Power_int
20:17:36 Presenting theory Physical_Quantities.Enum_extra
20:17:36 Presenting theory Physical_Quantities.Groups_mult
20:17:36 Presenting theory Physical_Quantities.ISQ_Dimensions
20:17:36 Presenting theory Physical_Quantities.ISQ_Quantities
20:17:36 Presenting theory Physical_Quantities.ISQ_Proof
20:17:36 Presenting theory Physical_Quantities.ISQ_Algebra
20:17:36 Presenting theory Physical_Quantities.ISQ_Units
20:17:36 Presenting theory Physical_Quantities.ISQ_Conversion
20:17:36 Presenting theory Physical_Quantities.ISQ
20:17:36 Presenting theory Physical_Quantities.SI_Units
20:17:36 Presenting theory Physical_Quantities.CGS
20:17:36 Presenting theory Physical_Quantities.SI_Constants
20:17:36 Presenting theory Physical_Quantities.SI_Prefix
20:17:36 Presenting theory Physical_Quantities.SI_Derived
20:17:36 Presenting theory Physical_Quantities.SI_Accepted
20:17:36 Presenting theory Physical_Quantities.SI_Imperial
20:17:36 Presenting theory Physical_Quantities.SI
20:17:36 Presenting theory Physical_Quantities.SI_Astronomical
20:17:36 Presenting theory Physical_Quantities.SI_Pretty
20:17:36 Presenting theory Physical_Quantities.BIS
20:17:36 Presenting Pop_Refinement ...
20:17:36 Presenting document Pop_Refinement/document
20:17:36 Presenting document Pop_Refinement/outline
20:17:36 Presenting theory Pop_Refinement.Definition
20:17:36 Presenting theory Pop_Refinement.First_Example
20:17:36 Presenting theory Pop_Refinement.Second_Example
20:17:36 Presenting theory Pop_Refinement.General_Remarks
20:17:36 Presenting theory Pop_Refinement.Related_Work
20:17:36 Presenting theory Pop_Refinement.Future_Work
20:17:36 Presenting Possibilistic_Noninterference ...
20:17:36 Presenting document Possibilistic_Noninterference/document
20:17:36 Presenting document Possibilistic_Noninterference/outline
20:17:36 Presenting theory Possibilistic_Noninterference.MyTactics
20:17:36 Presenting theory Possibilistic_Noninterference.Interface
20:17:36 Presenting theory Possibilistic_Noninterference.Bisim
20:17:36 Presenting theory Possibilistic_Noninterference.Language_Semantics
20:17:36 Presenting theory Possibilistic_Noninterference.During_Execution
20:17:36 Presenting theory Possibilistic_Noninterference.Compositionality
20:17:36 Presenting theory Possibilistic_Noninterference.Syntactic_Criteria
20:17:36 Presenting theory Possibilistic_Noninterference.After_Execution
20:17:36 Presenting theory Possibilistic_Noninterference.Concrete
20:17:37 Presenting Priority_Search_Trees ...
20:17:37 Presenting document Priority_Search_Trees/document
20:17:37 Presenting document Priority_Search_Trees/outline
20:17:37 Presenting theory Priority_Search_Trees.Prio_Map_Specs
20:17:37 Presenting theory Priority_Search_Trees.PST_General
20:17:37 Presenting theory Priority_Search_Trees.PST_RBT
20:17:37 Presenting Prim_Dijkstra_Simple ...
20:17:37 Presenting document Prim_Dijkstra_Simple/document
20:17:37 Presenting document Prim_Dijkstra_Simple/outline
20:17:37 Presenting theory Prim_Dijkstra_Simple.Common
20:17:37 Presenting theory Prim_Dijkstra_Simple.Chapter_Prim
20:17:37 Presenting theory Prim_Dijkstra_Simple.Undirected_Graph
20:17:37 Presenting theory Prim_Dijkstra_Simple.Undirected_Graph_Specs
20:17:37 Presenting theory Prim_Dijkstra_Simple.Prim_Abstract
20:17:37 Presenting theory Prim_Dijkstra_Simple.Undirected_Graph_Impl
20:17:37 Presenting theory Prim_Dijkstra_Simple.Prim_Impl
20:17:37 Presenting theory Prim_Dijkstra_Simple.Chapter_Dijkstra
20:17:37 Presenting theory Prim_Dijkstra_Simple.Directed_Graph
20:17:37 Presenting theory Prim_Dijkstra_Simple.Directed_Graph_Specs
20:17:37 Presenting theory Prim_Dijkstra_Simple.Dijkstra_Abstract
20:17:37 Presenting theory Prim_Dijkstra_Simple.Directed_Graph_Impl
20:17:38 Presenting theory Prim_Dijkstra_Simple.Dijkstra_Impl
20:17:38 Presenting Projective_Geometry ...
20:17:38 Presenting document Projective_Geometry/document
20:17:38 Presenting document Projective_Geometry/outline
20:17:38 Presenting theory Projective_Geometry.Projective_Plane_Axioms
20:17:38 Presenting theory Projective_Geometry.Pappus_Property
20:17:38 Presenting theory Projective_Geometry.Pascal_Property
20:17:38 Presenting theory Projective_Geometry.Desargues_Property
20:17:38 Presenting theory Projective_Geometry.Pappus_Desargues
20:17:38 Presenting theory Projective_Geometry.Higher_Projective_Space_Rank_Axioms
20:17:38 Presenting theory Projective_Geometry.Matroid_Rank_Properties
20:17:38 Presenting theory Projective_Geometry.Desargues_2D
20:17:38 Presenting theory Projective_Geometry.Desargues_3D
20:17:38 Presenting theory Projective_Geometry.Projective_Space_Axioms
20:17:38 Presenting theory Projective_Geometry.Higher_Projective_Space_Axioms
20:17:38 Presenting Proof_Strategy_Language ...
20:17:38 Presenting document Proof_Strategy_Language/document
20:17:38 Presenting document Proof_Strategy_Language/outline
20:17:38 Presenting theory Proof_Strategy_Language.Try_Hard
20:17:38 Presenting theory Proof_Strategy_Language.PSL
20:17:38 Presenting theory Proof_Strategy_Language.Example
20:17:39 Presenting file "Utils.ML"
20:17:39 Presenting file "Subtool.ML"
20:17:39 Presenting file "Dynamic_Tactic_Generation.ML"
20:17:39 Presenting file "Constructor_Class.ML"
20:17:39 Presenting file "Instantiation.ML"
20:17:39 Presenting file "Monadic_Prover.ML"
20:17:39 Presenting file "Parser_Combinator.ML"
20:17:39 Presenting file "PSL_Parser.ML"
20:17:39 Presenting file "Isar_Interface.ML"
20:17:39 Presenting PropResPI ...
20:17:39 Presenting document PropResPI/document
20:17:39 Presenting document PropResPI/outline
20:17:39 Presenting theory PropResPI.Propositional_Resolution
20:17:39 Presenting theory PropResPI.Prime_Implicates
20:17:40 Presenting Propositional_Proof_Systems ...
20:17:40 Presenting document Propositional_Proof_Systems/document
20:17:40 Presenting document Propositional_Proof_Systems/outline
20:17:40 Presenting theory Propositional_Proof_Systems.Formulas
20:17:40 Presenting theory Propositional_Proof_Systems.Sema
20:17:40 Presenting theory Propositional_Proof_Systems.Substitution
20:17:40 Presenting theory Propositional_Proof_Systems.Substitution_Sema
20:17:40 Presenting theory Propositional_Proof_Systems.CNF
20:17:40 Presenting theory Propositional_Proof_Systems.CNF_Formulas
20:17:40 Presenting theory Propositional_Proof_Systems.CNF_Sema
20:17:40 Presenting theory Propositional_Proof_Systems.CNF_Formulas_Sema
20:17:40 Presenting theory Propositional_Proof_Systems.CNF_To_Formula
20:17:40 Presenting theory Propositional_Proof_Systems.Tseytin
20:17:40 Presenting theory Propositional_Proof_Systems.Tseytin_Sema
20:17:40 Presenting theory Propositional_Proof_Systems.MiniFormulas
20:17:40 Presenting theory Propositional_Proof_Systems.MiniFormulas_Sema
20:17:40 Presenting theory Propositional_Proof_Systems.Consistency
20:17:40 Presenting theory Propositional_Proof_Systems.Compactness
20:17:40 Presenting theory Propositional_Proof_Systems.Compactness_Consistency
20:17:40 Presenting theory Propositional_Proof_Systems.Sema_Craig
20:17:40 Presenting theory Propositional_Proof_Systems.SC
20:17:40 Presenting theory Propositional_Proof_Systems.SC_Cut
20:17:40 Presenting theory Propositional_Proof_Systems.SC_Depth
20:17:40 Presenting theory Propositional_Proof_Systems.SC_Gentzen
20:17:40 Presenting theory Propositional_Proof_Systems.SC_Sema
20:17:40 Presenting theory Propositional_Proof_Systems.SC_Depth_Limit
20:17:40 Presenting theory Propositional_Proof_Systems.SC_Compl_Consistency
20:17:40 Presenting theory Propositional_Proof_Systems.ND
20:17:40 Presenting theory Propositional_Proof_Systems.ND_Sound
20:17:40 Presenting theory Propositional_Proof_Systems.ND_Compl_Truthtable
20:17:40 Presenting theory Propositional_Proof_Systems.ND_Compl_Truthtable_Compact
20:17:40 Presenting theory Propositional_Proof_Systems.HC
20:17:40 Presenting theory Propositional_Proof_Systems.HC_Compl_Consistency
20:17:40 Presenting theory Propositional_Proof_Systems.Resolution
20:17:40 Presenting theory Propositional_Proof_Systems.Resolution_Sound
20:17:40 Presenting theory Propositional_Proof_Systems.Resolution_Compl
20:17:40 Presenting theory Propositional_Proof_Systems.Resolution_Compl_Consistency
20:17:40 Presenting theory Propositional_Proof_Systems.HCSC
20:17:40 Presenting theory Propositional_Proof_Systems.SCND
20:17:40 Presenting theory Propositional_Proof_Systems.NDHC
20:17:40 Presenting theory Propositional_Proof_Systems.HCSCND
20:17:40 Presenting theory Propositional_Proof_Systems.LSC
20:17:40 Presenting theory Propositional_Proof_Systems.LSC_Resolution
20:17:40 Presenting theory Propositional_Proof_Systems.ND_FiniteAssms
20:17:40 Presenting theory Propositional_Proof_Systems.ND_Compl_SC
20:17:40 Presenting theory Propositional_Proof_Systems.Resolution_Compl_SC_Small
20:17:40 Presenting theory Propositional_Proof_Systems.Resolution_Compl_SC_Full
20:17:40 Presenting theory Propositional_Proof_Systems.MiniSC
20:17:40 Presenting theory Propositional_Proof_Systems.MiniSC_HC
20:17:40 Presenting theory Propositional_Proof_Systems.MiniSC_Craig
20:17:41 Presenting PseudoHoops ...
20:17:41 Presenting document PseudoHoops/document
20:17:41 Presenting document PseudoHoops/outline
20:17:41 Presenting theory PseudoHoops.Operations
20:17:41 Presenting theory PseudoHoops.LeftComplementedMonoid
20:17:41 Presenting theory PseudoHoops.RightComplementedMonoid
20:17:41 Presenting theory PseudoHoops.PseudoHoops
20:17:41 Presenting theory PseudoHoops.PseudoHoopFilters
20:17:41 Presenting theory PseudoHoops.PseudoWaisbergAlgebra
20:17:41 Presenting theory PseudoHoops.SpecialPseudoHoops
20:17:41 Presenting theory PseudoHoops.Examples
20:17:42 Presenting Ramsey-Infinite ...
20:17:42 Presenting document Ramsey-Infinite/document
20:17:42 Presenting document Ramsey-Infinite/outline
20:17:42 Presenting theory Ramsey-Infinite.Ramsey
20:17:42 Presenting Recursion-Theory-I ...
20:17:42 Presenting document Recursion-Theory-I/document
20:17:42 Presenting document Recursion-Theory-I/outline
20:17:42 Presenting theory Recursion-Theory-I.CPair
20:17:42 Presenting theory Recursion-Theory-I.PRecFun
20:17:42 Presenting theory Recursion-Theory-I.PRecList
20:17:42 Presenting theory Recursion-Theory-I.PRecFun2
20:17:42 Presenting theory Recursion-Theory-I.PRecFinSet
20:17:42 Presenting theory Recursion-Theory-I.PRecUnGr
20:17:42 Presenting theory Recursion-Theory-I.RecEnSet
20:17:43 Presenting file "Utils.ML"
20:17:43 Presenting RefinementReactive ...
20:17:43 Presenting document RefinementReactive/document
20:17:43 Presenting document RefinementReactive/outline
20:17:43 Presenting theory RefinementReactive.Temporal
20:17:43 Presenting theory RefinementReactive.Refinement
20:17:43 Presenting theory RefinementReactive.Reactive
20:17:43 Presenting Regex_Equivalence ...
20:17:43 Presenting document Regex_Equivalence/document
20:17:43 Presenting document Regex_Equivalence/outline
20:17:43 Presenting theory Regex_Equivalence.Automaton
20:17:43 Presenting theory Regex_Equivalence.Derivatives_Finite
20:17:43 Presenting theory Regex_Equivalence.Deriv_PDeriv
20:17:43 Presenting theory Regex_Equivalence.Deriv_Autos
20:17:43 Presenting theory Regex_Equivalence.Position_Autos
20:17:43 Presenting theory Regex_Equivalence.After2
20:17:43 Presenting theory Regex_Equivalence.Before2
20:17:43 Presenting theory Regex_Equivalence.Regex_Equivalence
20:17:43 Presenting theory Regex_Equivalence.Examples
20:17:43 Presenting theory Regex_Equivalence.Benchmark
20:17:44 Presenting Relational_Method ...
20:17:44 Presenting document Relational_Method/document
20:17:44 Presenting document Relational_Method/outline
20:17:44 Presenting theory Relational_Method.Definitions
20:17:44 Presenting theory Relational_Method.Authentication
20:17:44 Presenting theory Relational_Method.Anonymity
20:17:44 Presenting theory Relational_Method.Possibility
20:17:45 Presenting Resolution_FOL ...
20:17:45 Presenting document Resolution_FOL/document
20:17:45 Presenting document Resolution_FOL/outline
20:17:45 Presenting theory Resolution_FOL.TermsAndLiterals
20:17:45 Presenting theory Resolution_FOL.Tree
20:17:45 Presenting theory Resolution_FOL.Resolution
20:17:45 Presenting theory Resolution_FOL.Completeness
20:17:45 Presenting theory Resolution_FOL.Examples
20:17:45 Presenting theory Resolution_FOL.Unification_Theorem
20:17:45 Presenting theory Resolution_FOL.Completeness_Instance
20:17:45 Presenting Robbins-Conjecture ...
20:17:45 Presenting document Robbins-Conjecture/document
20:17:45 Presenting document Robbins-Conjecture/outline
20:17:45 Presenting theory Robbins-Conjecture.Robbins_Conjecture
20:17:45 Presenting Roy_Floyd_Warshall ...
20:17:45 Presenting document Roy_Floyd_Warshall/document
20:17:45 Presenting document Roy_Floyd_Warshall/outline
20:17:45 Presenting theory Roy_Floyd_Warshall.Roy_Floyd_Warshall
20:17:45 Presenting SIFPL ...
20:17:45 Presenting document SIFPL/document
20:17:45 Presenting document SIFPL/outline
20:17:45 Presenting theory SIFPL.IMP
20:17:45 Presenting theory SIFPL.VDM
20:17:45 Presenting theory SIFPL.VS
20:17:45 Presenting theory SIFPL.ContextVS
20:17:45 Presenting theory SIFPL.Lattice
20:17:45 Presenting theory SIFPL.HuntSands
20:17:45 Presenting theory SIFPL.OBJ
20:17:45 Presenting theory SIFPL.VDM_OBJ
20:17:45 Presenting theory SIFPL.PBIJ
20:17:45 Presenting theory SIFPL.VS_OBJ
20:17:46 Presenting theory SIFPL.ContextOBJ
20:17:47 Presenting SIFUM_Type_Systems ...
20:17:47 Presenting document SIFUM_Type_Systems/document
20:17:47 Presenting document SIFUM_Type_Systems/outline
20:17:47 Presenting theory SIFUM_Type_Systems.Preliminaries
20:17:47 Presenting theory SIFUM_Type_Systems.Security
20:17:47 Presenting theory SIFUM_Type_Systems.Compositionality
20:17:47 Presenting theory SIFUM_Type_Systems.Language
20:17:47 Presenting theory SIFUM_Type_Systems.TypeSystem
20:17:47 Presenting theory SIFUM_Type_Systems.LocallySoundModeUse
20:17:48 Presenting SPARCv8 ...
20:17:48 Presenting document SPARCv8/document
20:17:48 Presenting document SPARCv8/outline
20:17:48 Presenting theory SPARCv8.WordDecl
20:17:48 Presenting theory SPARCv8.Sparc_Types
20:17:48 Presenting theory SPARCv8.Lib
20:17:48 Presenting theory SPARCv8.DetMonadLemmas
20:17:48 Presenting theory SPARCv8.DetMonad
20:17:48 Presenting theory SPARCv8.RegistersOps
20:17:48 Presenting theory SPARCv8.MMU
20:17:48 Presenting theory SPARCv8.Sparc_State
20:17:48 Presenting theory SPARCv8.Sparc_Instruction
20:17:48 Presenting theory SPARCv8.Sparc_Execution
20:17:48 Presenting theory SPARCv8.Sparc_Properties
20:17:48 Presenting theory SPARCv8.Sparc_Init_State
20:17:48 Presenting theory SPARCv8.Sparc_Code_Gen
20:17:53 Presenting Schutz_Spacetime ...
20:17:53 Presenting document Schutz_Spacetime/document
20:17:53 Presenting document Schutz_Spacetime/outline
20:17:53 Presenting theory Schutz_Spacetime.Util
20:17:53 Presenting theory Schutz_Spacetime.TernaryOrdering
20:17:53 Presenting theory Schutz_Spacetime.Minkowski
20:17:53 Presenting theory Schutz_Spacetime.TemporalOrderOnPath
20:17:55 Presenting Security_Protocol_Refinement ...
20:17:55 Presenting document Security_Protocol_Refinement/document
20:17:55 Presenting document Security_Protocol_Refinement/outline
20:17:55 Presenting theory Security_Protocol_Refinement.Infra
20:17:55 Presenting theory Security_Protocol_Refinement.Refinement
20:17:55 Presenting theory Security_Protocol_Refinement.Agents
20:17:55 Presenting theory Security_Protocol_Refinement.Keys
20:17:55 Presenting theory Security_Protocol_Refinement.Atoms
20:17:55 Presenting theory Security_Protocol_Refinement.Runs
20:17:55 Presenting theory Security_Protocol_Refinement.Channels
20:17:55 Presenting theory Security_Protocol_Refinement.Message
20:17:55 Presenting theory Security_Protocol_Refinement.s0g_secrecy
20:17:55 Presenting theory Security_Protocol_Refinement.a0n_agree
20:17:55 Presenting theory Security_Protocol_Refinement.a0i_agree
20:17:55 Presenting theory Security_Protocol_Refinement.m1_auth
20:17:55 Presenting theory Security_Protocol_Refinement.m2_auth_chan
20:17:55 Presenting theory Security_Protocol_Refinement.m2_confid_chan
20:17:55 Presenting theory Security_Protocol_Refinement.m3_sig
20:17:55 Presenting theory Security_Protocol_Refinement.m3_enc
20:17:55 Presenting theory Security_Protocol_Refinement.m1_keydist
20:17:55 Presenting theory Security_Protocol_Refinement.m1_keydist_iirn
20:17:55 Presenting theory Security_Protocol_Refinement.m1_keydist_inrn
20:17:55 Presenting theory Security_Protocol_Refinement.m1_kerberos
20:17:55 Presenting theory Security_Protocol_Refinement.m2_kerberos
20:17:55 Presenting theory Security_Protocol_Refinement.m3_kerberos_par
20:17:55 Presenting theory Security_Protocol_Refinement.m3_kerberos5
20:17:56 Presenting theory Security_Protocol_Refinement.m3_kerberos4
20:17:56 Presenting theory Security_Protocol_Refinement.m1_nssk
20:17:56 Presenting theory Security_Protocol_Refinement.m2_nssk
20:17:56 Presenting theory Security_Protocol_Refinement.m3_nssk_par
20:17:56 Presenting theory Security_Protocol_Refinement.m3_nssk
20:17:56 Presenting theory Security_Protocol_Refinement.m1_ds
20:17:56 Presenting theory Security_Protocol_Refinement.m2_ds
20:17:56 Presenting theory Security_Protocol_Refinement.m3_ds_par
20:17:56 Presenting theory Security_Protocol_Refinement.m3_ds
20:17:57 Presenting SenSocialChoice ...
20:17:57 Presenting document SenSocialChoice/document
20:17:57 Presenting document SenSocialChoice/outline
20:17:57 Presenting theory SenSocialChoice.FSext
20:17:57 Presenting theory SenSocialChoice.RPRs
20:17:57 Presenting theory SenSocialChoice.SCFs
20:17:57 Presenting theory SenSocialChoice.Arrow
20:17:57 Presenting theory SenSocialChoice.Sen
20:17:57 Presenting theory SenSocialChoice.May
20:17:57 Presenting Separation_Algebra ...
20:17:57 Presenting document Separation_Algebra/document
20:17:57 Presenting document Separation_Algebra/outline
20:17:57 Presenting theory Separation_Algebra.Separation_Algebra
20:17:57 Presenting theory Separation_Algebra.Sep_Heap_Instance
20:17:57 Presenting theory Separation_Algebra.Sep_Tactics
20:17:57 Presenting theory Separation_Algebra.Simple_Separation_Example
20:17:57 Presenting theory Separation_Algebra.Sep_Tactics_Test
20:17:57 Presenting theory Separation_Algebra.Map_Extra
20:17:57 Presenting theory Separation_Algebra.VM_Example
20:17:57 Presenting theory Separation_Algebra.Separation_Algebra_Alt
20:17:57 Presenting theory Separation_Algebra.Sep_Eq
20:17:57 Presenting theory Separation_Algebra.Types_D
20:17:57 Presenting theory Separation_Algebra.Abstract_Separation_D
20:17:57 Presenting theory Separation_Algebra.Separation_D
20:17:57 Presenting file "sep_tactics.ML"
20:17:57 Presenting Simpl ...
20:17:57 Presenting document Simpl/document
20:17:57 Presenting document Simpl/outline
20:17:57 Presenting theory Simpl.Language
20:17:57 Presenting theory Simpl.Semantic
20:17:57 Presenting theory Simpl.HoarePartialDef
20:17:57 Presenting theory Simpl.HoarePartialProps
20:17:57 Presenting theory Simpl.HoarePartial
20:17:57 Presenting theory Simpl.Termination
20:17:57 Presenting theory Simpl.SmallStep
20:17:57 Presenting theory Simpl.HoareTotalDef
20:17:57 Presenting theory Simpl.HoareTotalProps
20:17:58 Presenting theory Simpl.HoareTotal
20:17:58 Presenting theory Simpl.Hoare
20:17:58 Presenting theory Simpl.StateSpace
20:17:58 Presenting theory Simpl.AlternativeSmallStep
20:18:00 Presenting theory Simpl.Simpl_Heap
20:18:00 Presenting theory Simpl.HeapList
20:18:00 Presenting theory Simpl.Generalise
20:18:00 Presenting theory Simpl.Vcg
20:18:00 Presenting file "generalise_state.ML"
20:18:00 Presenting theory Simpl.SyntaxTest
20:18:00 Presenting theory Simpl.VcgEx
20:18:01 Presenting theory Simpl.VcgExSP
20:18:01 Presenting theory Simpl.VcgExTotal
20:18:01 Presenting theory Simpl.Quicksort
20:18:01 Presenting theory Simpl.XVcg
20:18:01 Presenting theory Simpl.XVcgEx
20:18:01 Presenting theory Simpl.ProcParEx
20:18:01 Presenting theory Simpl.ProcParExSP
20:18:01 Presenting theory Simpl.Closure
20:18:02 Presenting theory Simpl.ClosureEx
20:18:02 Presenting theory Simpl.Compose
20:18:02 Presenting theory Simpl.ComposeEx
20:18:02 Presenting theory Simpl.UserGuide
20:18:02 Presenting theory Simpl.Simpl
20:18:03 Presenting file "hoare.ML"
20:18:03 Presenting file "hoare_syntax.ML"
20:18:04 Presenting BDD ...
20:18:04 Presenting document BDD/document
20:18:04 Presenting document BDD/outline
20:18:04 Presenting theory BDD.BinDag
20:18:04 Presenting theory BDD.General
20:18:04 Presenting theory BDD.ProcedureSpecs
20:18:04 Presenting theory BDD.EvalProof
20:18:04 Presenting theory BDD.LevellistProof
20:18:04 Presenting theory BDD.ShareRepProof
20:18:04 Presenting theory BDD.ShareReduceRepListProof
20:18:04 Presenting theory BDD.RepointProof
20:18:04 Presenting theory BDD.NormalizeTotalProof
20:18:05 Presenting Planarity_Certificates ...
20:18:05 Presenting document Planarity_Certificates/document
20:18:05 Presenting document Planarity_Certificates/outline
20:18:05 Presenting theory Planarity_Certificates.Lib
20:18:05 Presenting theory Planarity_Certificates.OptionMonad
20:18:05 Presenting theory Planarity_Certificates.NonDetMonad
20:18:05 Presenting theory Planarity_Certificates.NonDetMonadLemmas
20:18:05 Presenting theory Planarity_Certificates.OptionMonadND
20:18:05 Presenting theory Planarity_Certificates.WP
20:18:05 Presenting theory Planarity_Certificates.OptionMonadWP
20:18:05 Presenting theory Planarity_Certificates.Graph_Genus
20:18:05 Presenting theory Planarity_Certificates.List_Aux
20:18:05 Presenting theory Planarity_Certificates.Executable_Permutations
20:18:05 Presenting theory Planarity_Certificates.Digraph_Map_Impl
20:18:06 Presenting theory Planarity_Certificates.Planar_Complete
20:18:06 Presenting theory Planarity_Certificates.Reachablen
20:18:06 Presenting theory Planarity_Certificates.Permutations_2
20:18:06 Presenting theory Planarity_Certificates.Planar_Subdivision
20:18:06 Presenting theory Planarity_Certificates.Planar_Subgraph
20:18:06 Presenting theory Planarity_Certificates.Kuratowski_Combinatorial
20:18:06 Presenting theory Planarity_Certificates.Simpl_Anno
20:18:06 Presenting theory Planarity_Certificates.Check_Non_Planarity_Impl
20:18:06 Presenting theory Planarity_Certificates.Check_Non_Planarity_Verification
20:18:06 Presenting file "WP-method.ML"
20:18:06 Presenting theory Planarity_Certificates.AutoCorres_Misc
20:18:06 Presenting theory Planarity_Certificates.Setup_AutoCorres
20:18:06 Presenting theory Planarity_Certificates.Check_Planarity_Verification
20:18:06 Presenting theory Planarity_Certificates.Planarity_Certificates
20:18:06 Presenting file "$AFP/Case_Labeling/util.ML"
20:18:07 Presenting Sliding_Window_Algorithm ...
20:18:07 Presenting document Sliding_Window_Algorithm/document
20:18:07 Presenting document Sliding_Window_Algorithm/outline
20:18:07 Presenting theory Sliding_Window_Algorithm.SWA
20:18:07 Presenting Statecharts ...
20:18:07 Presenting document Statecharts/document
20:18:07 Presenting document Statecharts/outline
20:18:07 Presenting theory Statecharts.Contrib
20:18:07 Presenting theory Statecharts.DataSpace
20:18:07 Presenting theory Statecharts.Data
20:18:07 Presenting theory Statecharts.Update
20:18:07 Presenting theory Statecharts.Expr
20:18:07 Presenting theory Statecharts.SA
20:18:07 Presenting theory Statecharts.HA
20:18:07 Presenting theory Statecharts.HASem
20:18:07 Presenting theory Statecharts.Kripke
20:18:07 Presenting theory Statecharts.HAKripke
20:18:07 Presenting theory Statecharts.HAOps
20:18:07 Presenting theory Statecharts.CarAudioSystem
20:18:08 Presenting Stellar_Quorums ...
20:18:08 Presenting document Stellar_Quorums/document
20:18:08 Presenting document Stellar_Quorums/outline
20:18:08 Presenting theory Stellar_Quorums.Stellar_Quorums
20:18:08 Presenting Stone_Algebras ...
20:18:08 Presenting document Stone_Algebras/document
20:18:08 Presenting document Stone_Algebras/outline
20:18:08 Presenting theory Stone_Algebras.Lattice_Basics
20:18:08 Presenting theory Stone_Algebras.P_Algebras
20:18:08 Presenting theory Stone_Algebras.Filters
20:18:08 Presenting theory Stone_Algebras.Stone_Construction
20:18:09 Presenting Stone_Relation_Algebras ...
20:18:09 Presenting document Stone_Relation_Algebras/document
20:18:09 Presenting document Stone_Relation_Algebras/outline
20:18:09 Presenting theory Stone_Relation_Algebras.Fixpoints
20:18:09 Presenting theory Stone_Relation_Algebras.Semirings
20:18:09 Presenting theory Stone_Relation_Algebras.Relation_Algebras
20:18:09 Presenting theory Stone_Relation_Algebras.Relation_Subalgebras
20:18:09 Presenting theory Stone_Relation_Algebras.Matrix_Relation_Algebras
20:18:09 Presenting theory Stone_Relation_Algebras.Linear_Order_Matrices
20:18:09 Presenting Stone_Kleene_Relation_Algebras ...
20:18:09 Presenting document Stone_Kleene_Relation_Algebras/document
20:18:09 Presenting document Stone_Kleene_Relation_Algebras/outline
20:18:09 Presenting theory Stone_Kleene_Relation_Algebras.Iterings
20:18:09 Presenting theory Stone_Kleene_Relation_Algebras.Kleene_Algebras
20:18:09 Presenting theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras
20:18:09 Presenting theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Subalgebras
20:18:09 Presenting theory Stone_Kleene_Relation_Algebras.Matrix_Kleene_Algebras
20:18:10 Presenting Aggregation_Algebras ...
20:18:10 Presenting document Aggregation_Algebras/document
20:18:10 Presenting document Aggregation_Algebras/outline
20:18:10 Presenting theory Aggregation_Algebras.Semigroups_Big
20:18:10 Presenting theory Aggregation_Algebras.Aggregation_Algebras
20:18:10 Presenting theory Aggregation_Algebras.Matrix_Aggregation_Algebras
20:18:10 Presenting theory Aggregation_Algebras.Linear_Aggregation_Algebras
20:18:11 Presenting Relational_Minimum_Spanning_Trees ...
20:18:11 Presenting document Relational_Minimum_Spanning_Trees/document
20:18:11 Presenting document Relational_Minimum_Spanning_Trees/outline
20:18:11 Presenting theory Relational_Minimum_Spanning_Trees.Kruskal
20:18:11 Presenting theory Relational_Minimum_Spanning_Trees.Prim
20:18:11 Presenting theory Relational_Minimum_Spanning_Trees.Boruvka
20:18:11 Presenting Relational_Disjoint_Set_Forests ...
20:18:11 Presenting document Relational_Disjoint_Set_Forests/document
20:18:11 Presenting document Relational_Disjoint_Set_Forests/outline
20:18:11 Presenting theory Relational_Disjoint_Set_Forests.Disjoint_Set_Forests
20:18:11 Presenting theory Relational_Disjoint_Set_Forests.More_Disjoint_Set_Forests
20:18:12 Presenting Relational_Forests ...
20:18:12 Presenting document Relational_Forests/document
20:18:12 Presenting document Relational_Forests/outline
20:18:12 Presenting theory Relational_Forests.Forests
20:18:12 Presenting theory Relational_Forests.Algorithms
20:18:12 Presenting Subset_Boolean_Algebras ...
20:18:12 Presenting document Subset_Boolean_Algebras/document
20:18:12 Presenting document Subset_Boolean_Algebras/outline
20:18:12 Presenting theory Subset_Boolean_Algebras.Subset_Boolean_Algebras
20:18:13 Presenting Store_Buffer_Reduction ...
20:18:13 Presenting document Store_Buffer_Reduction/document
20:18:13 Presenting document Store_Buffer_Reduction/outline
20:18:13 Presenting theory Store_Buffer_Reduction.ReduceStoreBuffer
20:18:13 Presenting theory Store_Buffer_Reduction.ReduceStoreBufferSimulation
20:18:13 Presenting theory Store_Buffer_Reduction.PIMP
20:18:13 Presenting theory Store_Buffer_Reduction.SyntaxTweaks
20:18:13 Presenting theory Store_Buffer_Reduction.Abbrevs
20:18:13 Presenting theory Store_Buffer_Reduction.Variants
20:18:13 Presenting theory Store_Buffer_Reduction.Text
20:18:13 Presenting theory Store_Buffer_Reduction.Preliminaries
20:18:19 Presenting Strong_Security ...
20:18:19 Presenting document Strong_Security/document
20:18:19 Presenting document Strong_Security/outline
20:18:19 Presenting theory Strong_Security.Types
20:18:19 Presenting theory Strong_Security.Expr
20:18:19 Presenting theory Strong_Security.Domain_example
20:18:19 Presenting theory Strong_Security.MWLf
20:18:19 Presenting theory Strong_Security.Strong_Security
20:18:19 Presenting theory Strong_Security.Up_To_Technique
20:18:19 Presenting theory Strong_Security.Parallel_Composition
20:18:19 Presenting theory Strong_Security.Strongly_Secure_Skip_Assign
20:18:19 Presenting theory Strong_Security.Language_Composition
20:18:19 Presenting theory Strong_Security.Type_System
20:18:19 Presenting theory Strong_Security.Type_System_example
20:18:19 Presenting Sunflowers ...
20:18:19 Presenting document Sunflowers/document
20:18:19 Presenting document Sunflowers/outline
20:18:19 Presenting theory Sunflowers.Sunflower
20:18:19 Presenting theory Sunflowers.Erdos_Rado_Sunflower
20:18:19 Presenting Syntax_Independent_Logic ...
20:18:19 Presenting document Syntax_Independent_Logic/document
20:18:19 Presenting document Syntax_Independent_Logic/outline
20:18:19 Presenting theory Syntax_Independent_Logic.Prelim
20:18:19 Presenting theory Syntax_Independent_Logic.Syntax
20:18:19 Presenting theory Syntax_Independent_Logic.Deduction
20:18:19 Presenting theory Syntax_Independent_Logic.Natural_Deduction
20:18:19 Presenting theory Syntax_Independent_Logic.Pseudo_Term
20:18:19 Presenting theory Syntax_Independent_Logic.Standard_Model
20:18:19 Presenting theory Syntax_Independent_Logic.Syntax_Arith
20:18:19 Presenting theory Syntax_Independent_Logic.Deduction_Q
20:18:21 Presenting Goedel_Incompleteness ...
20:18:21 Presenting document Goedel_Incompleteness/document
20:18:21 Presenting document Goedel_Incompleteness/outline
20:18:21 Presenting theory Goedel_Incompleteness.Deduction2
20:18:21 Presenting theory Goedel_Incompleteness.Abstract_Encoding
20:18:21 Presenting theory Goedel_Incompleteness.Abstract_Representability
20:18:21 Presenting theory Goedel_Incompleteness.Diagonalization
20:18:21 Presenting theory Goedel_Incompleteness.Derivability_Conditions
20:18:21 Presenting theory Goedel_Incompleteness.Goedel_Formula
20:18:21 Presenting theory Goedel_Incompleteness.Standard_Model_More
20:18:21 Presenting theory Goedel_Incompleteness.Abstract_First_Goedel
20:18:21 Presenting theory Goedel_Incompleteness.Rosser_Formula
20:18:21 Presenting theory Goedel_Incompleteness.Abstract_First_Goedel_Rosser
20:18:21 Presenting theory Goedel_Incompleteness.Abstract_Second_Goedel
20:18:21 Presenting theory Goedel_Incompleteness.Abstract_Jeroslow_Encoding
20:18:21 Presenting theory Goedel_Incompleteness.Jeroslow_Original
20:18:21 Presenting theory Goedel_Incompleteness.Jeroslow_Simplified
20:18:21 Presenting theory Goedel_Incompleteness.Loeb_Formula
20:18:21 Presenting theory Goedel_Incompleteness.Loeb
20:18:21 Presenting theory Goedel_Incompleteness.Tarski
20:18:21 Presenting theory Goedel_Incompleteness.All_Abstract
20:18:21 Presenting Goedel_HFSet_Semantic ...
20:18:21 Presenting document Goedel_HFSet_Semantic/document
20:18:21 Presenting document Goedel_HFSet_Semantic/outline
20:18:21 Presenting theory Goedel_HFSet_Semantic.Instance
20:18:22 Presenting Goedel_HFSet_Semanticless ...
20:18:22 Presenting document Goedel_HFSet_Semanticless/document
20:18:22 Presenting document Goedel_HFSet_Semanticless/outline
20:18:22 Presenting theory Goedel_HFSet_Semanticless.SyntaxN
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Coding
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Predicates
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Sigma
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Coding_Predicates
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Pf_Predicates
20:18:22 Presenting theory Goedel_HFSet_Semanticless.II_Prelims
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Pseudo_Coding
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Quote
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Functions
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Goedel_I
20:18:22 Presenting theory Goedel_HFSet_Semanticless.Instance
20:18:24 Presenting Robinson_Arithmetic ...
20:18:24 Presenting document Robinson_Arithmetic/document
20:18:24 Presenting document Robinson_Arithmetic/outline
20:18:24 Presenting theory Robinson_Arithmetic.Robinson_Arithmetic
20:18:24 Presenting theory Robinson_Arithmetic.Instance
20:18:24 Presenting Szpilrajn ...
20:18:24 Presenting document Szpilrajn/document
20:18:24 Presenting document Szpilrajn/outline
20:18:24 Presenting theory Szpilrajn.Szpilrajn
20:18:24 Presenting TESL_Language ...
20:18:24 Presenting document TESL_Language/document
20:18:24 Presenting document TESL_Language/outline
20:18:24 Presenting theory TESL_Language.Introduction
20:18:24 Presenting theory TESL_Language.TESL
20:18:24 Presenting theory TESL_Language.Run
20:18:24 Presenting theory TESL_Language.Denotational
20:18:24 Presenting theory TESL_Language.SymbolicPrimitive
20:18:24 Presenting theory TESL_Language.Operational
20:18:24 Presenting theory TESL_Language.Corecursive_Prop
20:18:24 Presenting theory TESL_Language.Hygge_Theory
20:18:24 Presenting theory TESL_Language.StutteringDefs
20:18:24 Presenting theory TESL_Language.StutteringLemmas
20:18:25 Presenting theory TESL_Language.Stuttering
20:18:25 Presenting theory TESL_Language.Config_Morphisms
20:18:25 Presenting TLA ...
20:18:25 Presenting document TLA/document
20:18:25 Presenting document TLA/outline
20:18:25 Presenting theory TLA.Sequence
20:18:25 Presenting theory TLA.Intensional
20:18:25 Presenting theory TLA.Semantics
20:18:25 Presenting theory TLA.PreFormulas
20:18:25 Presenting theory TLA.Rules
20:18:25 Presenting theory TLA.Liveness
20:18:25 Presenting theory TLA.State
20:18:25 Presenting theory TLA.Even
20:18:25 Presenting theory TLA.Inc
20:18:25 Presenting theory TLA.Buffer
20:18:25 Presenting Timed_Automata ...
20:18:25 Presenting document Timed_Automata/document
20:18:25 Presenting document Timed_Automata/outline
20:18:25 Presenting theory Timed_Automata.Floyd_Warshall
20:18:25 Presenting theory Timed_Automata.Timed_Automata
20:18:25 Presenting theory Timed_Automata.DBM
20:18:25 Presenting theory Timed_Automata.Paths_Cycles
20:18:25 Presenting theory Timed_Automata.DBM_Basics
20:18:25 Presenting theory Timed_Automata.DBM_Operations
20:18:25 Presenting theory Timed_Automata.DBM_Zone_Semantics
20:18:25 Presenting theory Timed_Automata.Misc
20:18:25 Presenting theory Timed_Automata.DBM_Normalization
20:18:26 Presenting theory Timed_Automata.Regions_Beta
20:18:26 Presenting theory Timed_Automata.Regions
20:18:26 Presenting theory Timed_Automata.Closure
20:18:26 Presenting theory Timed_Automata.Approx_Beta
20:18:26 Presenting theory Timed_Automata.Normalized_Zone_Semantics
20:18:29 Presenting Topological_Semantics ...
20:18:29 Presenting document Topological_Semantics/document
20:18:29 Presenting document Topological_Semantics/outline
20:18:29 Presenting theory Topological_Semantics.sse_boolean_algebra
20:18:29 Presenting theory Topological_Semantics.sse_boolean_algebra_quantification
20:18:29 Presenting theory Topological_Semantics.sse_operation_positive
20:18:29 Presenting theory Topological_Semantics.sse_operation_positive_quantification
20:18:29 Presenting theory Topological_Semantics.sse_operation_negative
20:18:29 Presenting theory Topological_Semantics.sse_operation_negative_quantification
20:18:29 Presenting theory Topological_Semantics.topo_operators_basic
20:18:29 Presenting theory Topological_Semantics.topo_operators_derivative
20:18:29 Presenting theory Topological_Semantics.topo_alexandrov
20:18:29 Presenting theory Topological_Semantics.topo_frontier_algebra
20:18:29 Presenting theory Topological_Semantics.topo_negation_conditions
20:18:30 Presenting theory Topological_Semantics.topo_negation_fixedpoints
20:18:30 Presenting theory Topological_Semantics.ex_LFIs
20:18:30 Presenting theory Topological_Semantics.topo_strict_implication
20:18:30 Presenting theory Topological_Semantics.ex_subminimal_logics
20:18:30 Presenting theory Topological_Semantics.topo_derivative_algebra
20:18:30 Presenting theory Topological_Semantics.ex_LFUs
20:18:30 Presenting theory Topological_Semantics.topo_border_algebra
20:18:30 Presenting theory Topological_Semantics.topo_closure_algebra
20:18:30 Presenting theory Topological_Semantics.topo_interior_algebra
20:18:31 Presenting Transitive-Closure-II ...
20:18:31 Presenting document Transitive-Closure-II/document
20:18:31 Presenting document Transitive-Closure-II/outline
20:18:31 Presenting theory Transitive-Closure-II.RTrancl
20:18:31 Presenting Tree_Decomposition ...
20:18:31 Presenting document Tree_Decomposition/document
20:18:31 Presenting document Tree_Decomposition/outline
20:18:31 Presenting theory Tree_Decomposition.Graph
20:18:31 Presenting theory Tree_Decomposition.Tree
20:18:31 Presenting theory Tree_Decomposition.TreeDecomposition
20:18:31 Presenting theory Tree_Decomposition.TreewidthTree
20:18:31 Presenting theory Tree_Decomposition.TreewidthCompleteGraph
20:18:31 Presenting theory Tree_Decomposition.ExampleInstantiations
20:18:31 Presenting Types_Tableaus_and_Goedels_God ...
20:18:31 Presenting document Types_Tableaus_and_Goedels_God/document
20:18:31 Presenting document Types_Tableaus_and_Goedels_God/outline
20:18:31 Presenting theory Types_Tableaus_and_Goedels_God.Relations
20:18:31 Presenting theory Types_Tableaus_and_Goedels_God.IHOML
20:18:31 Presenting theory Types_Tableaus_and_Goedels_God.IHOML_Examples
20:18:31 Presenting theory Types_Tableaus_and_Goedels_God.GoedelProof_P1
20:18:31 Presenting theory Types_Tableaus_and_Goedels_God.GoedelProof_P2
20:18:31 Presenting theory Types_Tableaus_and_Goedels_God.FittingProof
20:18:31 Presenting theory Types_Tableaus_and_Goedels_God.AndersonProof
20:18:31 Presenting UPF ...
20:18:31 Presenting document UPF/document
20:18:31 Presenting document UPF/outline
20:18:31 Presenting theory UPF.Monads
20:18:31 Presenting theory UPF.UPFCore
20:18:31 Presenting theory UPF.ElementaryPolicies
20:18:31 Presenting theory UPF.SeqComposition
20:18:31 Presenting theory UPF.ParallelComposition
20:18:31 Presenting theory UPF.Normalisation
20:18:31 Presenting theory UPF.NormalisationTestSpecification
20:18:31 Presenting theory UPF.Analysis
20:18:31 Presenting theory UPF.UPF
20:18:31 Presenting theory UPF.Service
20:18:31 Presenting theory UPF.ServiceExample
20:18:32 Presenting UPF_Firewall ...
20:18:32 Presenting document UPF_Firewall/document
20:18:32 Presenting document UPF_Firewall/outline
20:18:32 Presenting theory UPF_Firewall.NetworkCore
20:18:32 Presenting theory UPF_Firewall.DatatypeAddress
20:18:32 Presenting theory UPF_Firewall.DatatypePort
20:18:32 Presenting theory UPF_Firewall.IntegerAddress
20:18:32 Presenting theory UPF_Firewall.IntegerPort
20:18:32 Presenting theory UPF_Firewall.IntegerPort_TCPUDP
20:18:32 Presenting theory UPF_Firewall.IPv4
20:18:32 Presenting theory UPF_Firewall.IPv4_TCPUDP
20:18:32 Presenting theory UPF_Firewall.NetworkModels
20:18:32 Presenting theory UPF_Firewall.PolicyCore
20:18:32 Presenting theory UPF_Firewall.PolicyCombinators
20:18:32 Presenting theory UPF_Firewall.PortCombinators
20:18:32 Presenting theory UPF_Firewall.ProtocolPortCombinators
20:18:32 Presenting theory UPF_Firewall.Ports
20:18:32 Presenting theory UPF_Firewall.PacketFilter
20:18:32 Presenting theory UPF_Firewall.NAT
20:18:32 Presenting theory UPF_Firewall.FWNormalisationCore
20:18:32 Presenting theory UPF_Firewall.NormalisationGenericProofs
20:18:32 Presenting theory UPF_Firewall.NormalisationIntegerPortProof
20:18:32 Presenting theory UPF_Firewall.NormalisationIPPProofs
20:18:32 Presenting theory UPF_Firewall.ElementaryRules
20:18:32 Presenting theory UPF_Firewall.FWNormalisation
20:18:32 Presenting theory UPF_Firewall.LTL_alike
20:18:32 Presenting theory UPF_Firewall.StatefulCore
20:18:32 Presenting theory UPF_Firewall.FTP
20:18:32 Presenting theory UPF_Firewall.FTP_WithPolicy
20:18:32 Presenting theory UPF_Firewall.VOIP
20:18:32 Presenting theory UPF_Firewall.FTPVOIP
20:18:32 Presenting theory UPF_Firewall.StatefulFW
20:18:32 Presenting theory UPF_Firewall.UPF-Firewall
20:18:32 Presenting theory UPF_Firewall.DMZDatatype
20:18:32 Presenting theory UPF_Firewall.DMZInteger
20:18:32 Presenting theory UPF_Firewall.DMZ
20:18:32 Presenting theory UPF_Firewall.Voice_over_IP
20:18:32 Presenting theory UPF_Firewall.Transformation01
20:18:32 Presenting theory UPF_Firewall.Transformation02
20:18:32 Presenting theory UPF_Firewall.Transformation
20:18:32 Presenting theory UPF_Firewall.NAT-FW
20:18:32 Presenting theory UPF_Firewall.PersonalFirewallInt
20:18:32 Presenting theory UPF_Firewall.PersonalFirewallIpv4
20:18:32 Presenting theory UPF_Firewall.PersonalFirewallDatatype
20:18:32 Presenting theory UPF_Firewall.PersonalFirewall
20:18:32 Presenting theory UPF_Firewall.Examples
20:18:34 Presenting Universal_Turing_Machine ...
20:18:34 Presenting document Universal_Turing_Machine/document
20:18:34 Presenting document Universal_Turing_Machine/outline
20:18:34 Presenting theory Universal_Turing_Machine.Turing
20:18:34 Presenting theory Universal_Turing_Machine.Turing_Hoare
20:18:34 Presenting theory Universal_Turing_Machine.Uncomputable
20:18:34 Presenting theory Universal_Turing_Machine.Abacus_Mopup
20:18:34 Presenting theory Universal_Turing_Machine.Abacus
20:18:34 Presenting theory Universal_Turing_Machine.Abacus_Defs
20:18:34 Presenting theory Universal_Turing_Machine.Rec_Def
20:18:34 Presenting theory Universal_Turing_Machine.Abacus_Hoare
20:18:34 Presenting theory Universal_Turing_Machine.Recursive
20:18:34 Presenting theory Universal_Turing_Machine.Recs
20:18:34 Presenting theory Universal_Turing_Machine.UF
20:18:34 Presenting theory Universal_Turing_Machine.UTM
20:18:37 Presenting Van_der_Waerden ...
20:18:37 Presenting document Van_der_Waerden/document
20:18:37 Presenting document Van_der_Waerden/outline
20:18:37 Presenting theory Van_der_Waerden.Digits
20:18:37 Presenting theory Van_der_Waerden.Van_der_Waerden
20:18:37 Presenting VeriComp ...
20:18:38 Presenting document VeriComp/document
20:18:38 Presenting document VeriComp/outline
20:18:38 Presenting theory VeriComp.Behaviour
20:18:38 Presenting theory VeriComp.Well_founded
20:18:38 Presenting theory VeriComp.Inf
20:18:38 Presenting theory VeriComp.Transfer_Extras
20:18:38 Presenting theory VeriComp.Semantics
20:18:38 Presenting theory VeriComp.Language
20:18:38 Presenting theory VeriComp.Simulation
20:18:38 Presenting theory VeriComp.Compiler
20:18:38 Presenting theory VeriComp.Fixpoint
20:18:38 Presenting Verified-Prover ...
20:18:38 Presenting document Verified-Prover/document
20:18:38 Presenting document Verified-Prover/outline
20:18:38 Presenting theory Verified-Prover.Prover
20:18:38 Presenting Verified_SAT_Based_AI_Planning ...
20:18:38 Presenting document Verified_SAT_Based_AI_Planning/document
20:18:38 Presenting document Verified_SAT_Based_AI_Planning/outline
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.List_Supplement
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.Map_Supplement
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.CNF_Supplement
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.CNF_Semantics_Supplement
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.State_Variable_Representation
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.STRIPS_Representation
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.STRIPS_Semantics
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.SAS_Plus_Representation
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.SAS_Plus_Semantics
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.SAS_Plus_STRIPS
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.SAT_Plan_Base
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.SAT_Plan_Extensions
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.SAT_Solve_SAS_Plus
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.AST_SAS_Plus_Equivalence
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.Set2_Join_RBT
20:18:38 Presenting theory Verified_SAT_Based_AI_Planning.Solve_SASP
20:18:40 Presenting VolpanoSmith ...
20:18:40 Presenting document VolpanoSmith/document
20:18:40 Presenting document VolpanoSmith/outline
20:18:40 Presenting theory VolpanoSmith.Semantics
20:18:40 Presenting theory VolpanoSmith.secTypes
20:18:40 Presenting theory VolpanoSmith.Execute
20:18:41 Presenting WHATandWHERE_Security ...
20:18:41 Presenting document WHATandWHERE_Security/document
20:18:41 Presenting document WHATandWHERE_Security/outline
20:18:41 Presenting theory WHATandWHERE_Security.WHATWHERE_Security
20:18:41 Presenting theory WHATandWHERE_Security.Up_To_Technique
20:18:41 Presenting theory WHATandWHERE_Security.MWLs
20:18:41 Presenting theory WHATandWHERE_Security.Parallel_Composition
20:18:41 Presenting theory WHATandWHERE_Security.WHATWHERE_Secure_Skip_Assign
20:18:41 Presenting theory WHATandWHERE_Security.Language_Composition
20:18:41 Presenting theory WHATandWHERE_Security.Type_System
20:18:41 Presenting theory WHATandWHERE_Security.Type_System_example
20:18:41 Presenting WOOT_Strong_Eventual_Consistency ...
20:18:41 Presenting document WOOT_Strong_Eventual_Consistency/document
20:18:41 Presenting document WOOT_Strong_Eventual_Consistency/outline
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.ErrorMonad
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.Data
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.BasicAlgorithms
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.CreateAlgorithms
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.IntegrateAlgorithm
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.DistributedExecution
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.SortKeys
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.Psi
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.Sorting
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.Consistency
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.CreateConsistent
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.IntegrateInsertCommute
20:18:41 Presenting theory WOOT_Strong_Eventual_Consistency.StrongConvergence
20:18:42 Presenting theory WOOT_Strong_Eventual_Consistency.SEC
20:18:42 Presenting theory WOOT_Strong_Eventual_Consistency.Example
20:18:42 Presenting Weight_Balanced_Trees ...
20:18:42 Presenting document Weight_Balanced_Trees/document
20:18:42 Presenting document Weight_Balanced_Trees/outline
20:18:42 Presenting theory Weight_Balanced_Trees.Weight_Balanced_Trees_log
20:18:42 Presenting theory Weight_Balanced_Trees.Weight_Balanced_Trees
20:18:42 Presenting Word_Lib ...
20:18:42 Presenting document Word_Lib/document
20:18:42 Presenting document Word_Lib/outline
20:18:42 Presenting theory Word_Lib.More_Arithmetic
20:18:42 Presenting theory Word_Lib.Even_More_List
20:18:42 Presenting theory Word_Lib.More_Sublist
20:18:42 Presenting theory Word_Lib.More_Misc
20:18:42 Presenting theory Word_Lib.More_Divides
20:18:42 Presenting theory Word_Lib.More_Word
20:18:42 Presenting theory Word_Lib.Strict_part_mono
20:18:42 Presenting theory Word_Lib.Many_More
20:18:42 Presenting theory Word_Lib.Bit_Comprehension
20:18:42 Presenting theory Word_Lib.Most_significant_bit
20:18:42 Presenting theory Word_Lib.Least_significant_bit
20:18:42 Presenting theory Word_Lib.Generic_set_bit
20:18:42 Presenting theory Word_Lib.Bits_Int
20:18:42 Presenting theory Word_Lib.Typedef_Morphisms
20:18:42 Presenting theory Word_Lib.Word_EqI
20:18:42 Presenting theory Word_Lib.Aligned
20:18:42 Presenting theory Word_Lib.Singleton_Bit_Shifts
20:18:42 Presenting theory Word_Lib.Legacy_Aliases
20:18:42 Presenting theory Word_Lib.Reversed_Bit_Lists
20:18:42 Presenting theory Word_Lib.Ancient_Numeral
20:18:42 Presenting theory Word_Lib.Bit_Shifts_Infix_Syntax
20:18:42 Presenting theory Word_Lib.Next_and_Prev
20:18:42 Presenting theory Word_Lib.Signed_Division_Word
20:18:42 Presenting theory Word_Lib.Bitwise
20:18:42 Presenting theory Word_Lib.Examples
20:18:42 Presenting theory Word_Lib.Signed_Words
20:18:42 Presenting theory Word_Lib.Bitwise_Signed
20:18:42 Presenting theory Word_Lib.Enumeration
20:18:43 Presenting theory Word_Lib.Enumeration_Word
20:18:43 Presenting theory Word_Lib.Hex_Words
20:18:43 Presenting theory Word_Lib.Norm_Words
20:18:43 Presenting theory Word_Lib.Rsplit
20:18:43 Presenting theory Word_Lib.Syntax_Bundles
20:18:43 Presenting theory Word_Lib.Type_Syntax
20:18:43 Presenting theory Word_Lib.Word_Lemmas
20:18:43 Presenting theory Word_Lib.Word_8
20:18:43 Presenting theory Word_Lib.Word_16
20:18:43 Presenting theory Word_Lib.Word_Syntax
20:18:43 Presenting theory Word_Lib.Word_Names
20:18:43 Presenting theory Word_Lib.More_Word_Operations
20:18:43 Presenting theory Word_Lib.Word_32
20:18:43 Presenting theory Word_Lib.Word_Lib_Sumo
20:18:43 Presenting theory Word_Lib.Word_64
20:18:43 Presenting theory Word_Lib.Guide
20:18:44 Presenting Complx ...
20:18:44 Presenting document Complx/document
20:18:44 Presenting document Complx/outline
20:18:44 Presenting theory Complx.Language
20:18:44 Presenting theory Complx.SmallStep
20:18:44 Presenting theory Complx.OG_Annotations
20:18:44 Presenting theory Complx.OG_Hoare
20:18:44 Presenting theory Complx.SeqCatch_decomp
20:18:44 Presenting theory Complx.OG_Soundness
20:18:44 Presenting theory Complx.Cache_Tactics
20:18:44 Presenting theory Complx.OG_Tactics
20:18:44 Presenting theory Complx.OG_Syntax
20:18:44 Presenting theory Complx.Examples
20:18:44 Presenting theory Complx.SumArr
20:18:45 Presenting IEEE_Floating_Point ...
20:18:45 Presenting document IEEE_Floating_Point/document
20:18:45 Presenting document IEEE_Floating_Point/outline
20:18:45 Presenting theory IEEE_Floating_Point.IEEE
20:18:45 Presenting theory IEEE_Floating_Point.IEEE_Properties
20:18:45 Presenting theory IEEE_Floating_Point.FP64
20:18:45 Presenting theory IEEE_Floating_Point.Conversion_IEEE_Float
20:18:45 Presenting theory IEEE_Floating_Point.Double
20:18:45 Presenting IP_Addresses ...
20:18:45 Presenting document IP_Addresses/document
20:18:45 Presenting document IP_Addresses/outline
20:18:45 Presenting theory IP_Addresses.NumberWang_IPv4
20:18:45 Presenting theory IP_Addresses.NumberWang_IPv6
20:18:45 Presenting theory IP_Addresses.WordInterval
20:18:45 Presenting theory IP_Addresses.Hs_Compat
20:18:45 Presenting theory IP_Addresses.IP_Address
20:18:45 Presenting theory IP_Addresses.IPv4
20:18:45 Presenting theory IP_Addresses.IPv6
20:18:45 Presenting theory IP_Addresses.Prefix_Match
20:18:45 Presenting theory IP_Addresses.CIDR_Split
20:18:45 Presenting theory IP_Addresses.WordInterval_Sorted
20:18:45 Presenting theory IP_Addresses.IP_Address_Parser
20:18:45 Presenting theory IP_Addresses.Lib_Numbers_toString
20:18:45 Presenting theory IP_Addresses.Lib_Word_toString
20:18:45 Presenting theory IP_Addresses.Lib_List_toString
20:18:45 Presenting theory IP_Addresses.IP_Address_toString
20:18:45 Presenting theory IP_Addresses.Prefix_Match_toString
20:18:46 Presenting Simple_Firewall ...
20:18:46 Presenting document Simple_Firewall/document
20:18:46 Presenting document Simple_Firewall/outline
20:18:46 Presenting theory Simple_Firewall.Lib_Enum_toString
20:18:46 Presenting theory Simple_Firewall.L4_Protocol
20:18:46 Presenting theory Simple_Firewall.Simple_Packet
20:18:46 Presenting theory Simple_Firewall.Firewall_Common_Decision_State
20:18:46 Presenting theory Simple_Firewall.Iface
20:18:46 Presenting theory Simple_Firewall.SimpleFw_Syntax
20:18:46 Presenting theory Simple_Firewall.SimpleFw_Semantics
20:18:46 Presenting theory Simple_Firewall.List_Product_More
20:18:46 Presenting theory Simple_Firewall.Option_Helpers
20:18:46 Presenting theory Simple_Firewall.Generic_SimpleFw
20:18:46 Presenting theory Simple_Firewall.Shadowed
20:18:46 Presenting theory Simple_Firewall.IP_Partition_Preliminaries
20:18:46 Presenting theory Simple_Firewall.GroupF
20:18:46 Presenting theory Simple_Firewall.IP_Addr_WordInterval_toString
20:18:46 Presenting theory Simple_Firewall.Primitives_toString
20:18:46 Presenting theory Simple_Firewall.Service_Matrix
20:18:46 Presenting theory Simple_Firewall.SimpleFw_toString
20:18:46 Presenting Routing ...
20:18:46 Presenting document Routing/document
20:18:46 Presenting document Routing/outline
20:18:46 Presenting theory Routing.Linorder_Helper
20:18:46 Presenting theory Routing.Routing_Table
20:18:46 Presenting theory Routing.Linux_Router
20:18:46 Presenting theory Routing.IpRoute_Parser
20:18:47 Presenting file "IpRoute_Parser.ml"
20:18:47 Presenting Iptables_Semantics ...
20:18:47 Presenting document Iptables_Semantics/document
20:18:47 Presenting document Iptables_Semantics/outline
20:18:47 Presenting theory Iptables_Semantics.List_Misc
20:18:47 Presenting theory Iptables_Semantics.Negation_Type
20:18:47 Presenting theory Iptables_Semantics.WordInterval_Lists
20:18:47 Presenting theory Iptables_Semantics.Repeat_Stabilize
20:18:47 Presenting theory Iptables_Semantics.Firewall_Common
20:18:47 Presenting theory Iptables_Semantics.Semantics
20:18:47 Presenting theory Iptables_Semantics.Matching
20:18:47 Presenting theory Iptables_Semantics.Ruleset_Update
20:18:47 Presenting theory Iptables_Semantics.Call_Return_Unfolding
20:18:47 Presenting theory Iptables_Semantics.Ternary
20:18:47 Presenting theory Iptables_Semantics.Matching_Ternary
20:18:47 Presenting theory Iptables_Semantics.Semantics_Ternary
20:18:47 Presenting theory Iptables_Semantics.Datatype_Selectors
20:18:47 Presenting theory Iptables_Semantics.IpAddresses
20:18:47 Presenting theory Iptables_Semantics.L4_Protocol_Flags
20:18:47 Presenting theory Iptables_Semantics.Ports
20:18:47 Presenting theory Iptables_Semantics.Conntrack_State
20:18:47 Presenting theory Iptables_Semantics.Tagged_Packet
20:18:47 Presenting theory Iptables_Semantics.Common_Primitive_Syntax
20:18:47 Presenting theory Iptables_Semantics.Unknown_Match_Tacs
20:18:47 Presenting theory Iptables_Semantics.Common_Primitive_Matcher_Generic
20:18:47 Presenting theory Iptables_Semantics.Common_Primitive_Matcher
20:18:47 Presenting theory Iptables_Semantics.Example_Semantics
20:18:47 Presenting theory Iptables_Semantics.Alternative_Semantics
20:18:47 Presenting theory Iptables_Semantics.Semantics_Stateful
20:18:47 Presenting theory Iptables_Semantics.Semantics_Goto
20:18:47 Presenting theory Iptables_Semantics.Negation_Type_DNF
20:18:47 Presenting theory Iptables_Semantics.Matching_Embeddings
20:18:48 Presenting theory Iptables_Semantics.Fixed_Action
20:18:48 Presenting theory Iptables_Semantics.Normalized_Matches
20:18:48 Presenting theory Iptables_Semantics.Negation_Type_Matching
20:18:48 Presenting theory Iptables_Semantics.Primitive_Normalization
20:18:48 Presenting theory Iptables_Semantics.MatchExpr_Fold
20:18:48 Presenting theory Iptables_Semantics.Common_Primitive_Lemmas
20:18:48 Presenting theory Iptables_Semantics.Ports_Normalize
20:18:48 Presenting theory Iptables_Semantics.IpAddresses_Normalize
20:18:48 Presenting theory Iptables_Semantics.Interfaces_Normalize
20:18:48 Presenting theory Iptables_Semantics.Word_Upto
20:18:48 Presenting theory Iptables_Semantics.Protocols_Normalize
20:18:48 Presenting theory Iptables_Semantics.Remdups_Rev
20:18:48 Presenting theory Iptables_Semantics.Ipassmt
20:18:48 Presenting theory Iptables_Semantics.No_Spoof
20:18:48 Presenting theory Iptables_Semantics.Common_Primitive_toString
20:18:48 Presenting theory Iptables_Semantics.Routing_IpAssmt
20:18:48 Presenting theory Iptables_Semantics.Output_Interface_Replace
20:18:48 Presenting theory Iptables_Semantics.Interface_Replace
20:18:48 Presenting theory Iptables_Semantics.Optimizing
20:18:48 Presenting theory Iptables_Semantics.Transform
20:18:49 Presenting theory Iptables_Semantics.Conntrack_State_Transform
20:18:49 Presenting theory Iptables_Semantics.Primitive_Abstract
20:18:49 Presenting theory Iptables_Semantics.SimpleFw_Compliance
20:18:49 Presenting theory Iptables_Semantics.Semantics_Embeddings
20:18:49 Presenting theory Iptables_Semantics.Iptables_Semantics
20:18:49 Presenting theory Iptables_Semantics.Code_Interface
20:18:49 Presenting theory Iptables_Semantics.Parser6
20:18:49 Presenting theory Iptables_Semantics.No_Spoof_Embeddings
20:18:49 Presenting theory Iptables_Semantics.Parser
20:18:49 Presenting theory Iptables_Semantics.Code_haskell
20:18:49 Presenting theory Iptables_Semantics.Access_Matrix_Embeddings
20:18:49 Presenting theory Iptables_Semantics.Documentation
20:18:50 Presenting Iptables_Semantics_Examples ...
20:18:50 Presenting document Iptables_Semantics_Examples/document
20:18:50 Presenting document Iptables_Semantics_Examples/outline
20:18:50 Presenting theory Iptables_Semantics_Examples.Parser_Test
20:18:50 Presenting theory Iptables_Semantics_Examples.Parser6_Test
20:18:50 Presenting theory Iptables_Semantics_Examples.Small_Examples
20:18:50 Presenting theory Iptables_Semantics_Examples.Ports_Fail
20:18:50 Presenting theory Iptables_Semantics_Examples.Contrived_Example
20:18:50 Presenting theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
20:18:50 Presenting theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
20:18:50 Presenting theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
20:18:50 Presenting theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
20:18:50 Presenting theory Iptables_Semantics_Examples.SQRL_2015_nospoof
20:18:50 Presenting theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
20:18:50 Presenting theory Iptables_Semantics_Examples.Analyze_medium_sized_company
20:18:51 Presenting LOFT ...
20:18:51 Presenting document LOFT/document
20:18:51 Presenting document LOFT/outline
20:18:51 Presenting theory LOFT.OpenFlow_Helpers
20:18:51 Presenting theory LOFT.Sort_Descending
20:18:51 Presenting theory LOFT.List_Group
20:18:51 Presenting theory LOFT.OpenFlow_Matches
20:18:51 Presenting theory LOFT.OpenFlow_Action
20:18:51 Presenting theory LOFT.Semantics_OpenFlow
20:18:51 Presenting theory LOFT.OpenFlow_Serialize
20:18:51 Presenting theory LOFT.Featherweight_OpenFlow_Comparison
20:18:51 Presenting theory LOFT.LinuxRouter_OpenFlow_Translation
20:18:51 Presenting theory LOFT.OF_conv_test
20:18:51 Presenting theory LOFT.RFC2544
20:18:51 Presenting theory LOFT.OpenFlow_Documentation
20:18:52 Presenting Interval_Arithmetic_Word32 ...
20:18:52 Presenting document Interval_Arithmetic_Word32/document
20:18:52 Presenting document Interval_Arithmetic_Word32/outline
20:18:52 Presenting theory Interval_Arithmetic_Word32.Interval_Word32
20:18:52 Presenting theory Interval_Arithmetic_Word32.Finite_String
20:18:52 Presenting theory Interval_Arithmetic_Word32.Interpreter
20:18:52 Presenting Native_Word ...
20:18:52 Presenting document Native_Word/document
20:18:52 Presenting document Native_Word/outline
20:18:52 Presenting theory Native_Word.Code_Int_Integer_Conversion
20:18:52 Presenting theory Native_Word.Code_Symbolic_Bits_Int
20:18:52 Presenting theory Native_Word.Bits_Integer
20:18:52 Presenting theory Native_Word.Code_Target_Word_Base
20:18:52 Presenting theory Native_Word.Word_Type_Copies
20:18:52 Presenting theory Native_Word.Uint64
20:18:52 Presenting theory Native_Word.Uint32
20:18:52 Presenting theory Native_Word.Uint16
20:18:52 Presenting theory Native_Word.Uint8
20:18:53 Presenting theory Native_Word.Uint
20:18:53 Presenting theory Native_Word.Native_Cast
20:18:53 Presenting theory Native_Word.Native_Cast_Uint
20:18:53 Presenting theory Native_Word.Native_Word_Imperative_HOL
20:18:53 Presenting theory Native_Word.Native_Word_Test
20:18:53 Presenting theory Native_Word.Code_Target_Bits_Int
20:18:53 Presenting theory Native_Word.Native_Word_Test_Emu
20:18:53 Presenting theory Native_Word.Native_Word_Test_PolyML
20:18:53 Presenting theory Native_Word.Native_Word_Test_PolyML2
20:18:53 Presenting theory Native_Word.Native_Word_Test_PolyML64
20:18:53 Presenting theory Native_Word.Native_Word_Test_Scala
20:18:53 Presenting theory Native_Word.Native_Word_Test_GHC
20:18:53 Presenting theory Native_Word.Native_Word_Test_MLton
20:18:53 Presenting theory Native_Word.Native_Word_Test_MLton2
20:18:53 Presenting theory Native_Word.Native_Word_Test_OCaml
20:18:53 Presenting theory Native_Word.Native_Word_Test_OCaml2
20:18:53 Presenting theory Native_Word.Native_Word_Test_SMLNJ
20:18:53 Presenting theory Native_Word.Native_Word_Test_SMLNJ2
20:18:53 Presenting theory Native_Word.Uint_Userguide
20:18:53 Presenting ZFC_in_HOL ...
20:18:53 Presenting document ZFC_in_HOL/document
20:18:53 Presenting document ZFC_in_HOL/outline
20:18:53 Presenting theory ZFC_in_HOL.ZFC_Library
20:18:53 Presenting theory ZFC_in_HOL.ZFC_in_HOL
20:18:53 Presenting theory ZFC_in_HOL.ZFC_Cardinals
20:18:53 Presenting theory ZFC_in_HOL.Kirby
20:18:53 Presenting theory ZFC_in_HOL.Ordinal_Exp
20:18:53 Presenting theory ZFC_in_HOL.Cantor_NF
20:18:53 Presenting theory ZFC_in_HOL.ZFC_Typeclasses
20:18:54 Presenting CZH_Foundations ...
20:18:54 Presenting document CZH_Foundations/document
20:18:54 Presenting document CZH_Foundations/outline
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_MIF
20:18:54 Presenting theory CZH_Foundations.CZH_Utilities
20:18:54 Presenting theory CZH_Foundations.CZH_Introduction
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_Introduction
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_Sets
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_Nat
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_BRelations
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_IF
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_Equipollence
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_Cardinality
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_Ordinals
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_FSequences
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_FBRelations
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_VNHS
20:18:54 Presenting theory CZH_Foundations.CZH_Sets_NOP
20:18:55 Presenting theory CZH_Foundations.HOL_CContinuum
20:18:55 Presenting theory CZH_Foundations.CZH_Sets_ZQR
20:18:55 Presenting theory CZH_Foundations.CZH_EX_Replacement
20:18:55 Presenting theory CZH_Foundations.CZH_EX_TS
20:18:55 Presenting theory CZH_Foundations.CZH_EX_Algebra
20:18:55 Presenting theory CZH_Foundations.CZH_Sets_Conclusions
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Introduction
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Digraph
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Small_Digraph
20:18:55 Presenting theory CZH_Foundations.CZH_DG_DGHM
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Small_DGHM
20:18:55 Presenting theory CZH_Foundations.CZH_DG_TDGHM
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Small_TDGHM
20:18:55 Presenting theory CZH_Foundations.CZH_DG_PDigraph
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Subdigraph
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Simple
20:18:55 Presenting theory CZH_Foundations.CZH_DG_GRPH
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Rel
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Par
20:18:55 Presenting theory CZH_Foundations.CZH_DG_Set
20:18:56 Presenting theory CZH_Foundations.CZH_DG_Conclusions
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Introduction
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Semicategory
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Small_Semicategory
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Semifunctor
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Small_Semifunctor
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_NTSMCF
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Small_NTSMCF
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_PSemicategory
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Subsemicategory
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Simple
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Rel
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Par
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_Set
20:18:56 Presenting theory CZH_Foundations.CZH_SMC_GRPH
20:18:57 Presenting theory CZH_Foundations.CZH_DG_SemiCAT
20:18:57 Presenting theory CZH_Foundations.CZH_SMC_SemiCAT
20:18:57 Presenting theory CZH_Foundations.CZH_SMC_Conclusions
20:18:57 Presenting CZH_Elementary_Categories ...
20:18:57 Presenting document CZH_Elementary_Categories/document
20:18:57 Presenting document CZH_Elementary_Categories/outline
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Introduction
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Category
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Small_Category
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Functor
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Small_Functor
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_NTCF
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Small_NTCF
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_PCategory
20:18:57 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Subcategory
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Simple
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Discrete
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_SS
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Parallel
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Comma
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Rel
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Par
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Set
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_GRPH
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_SemiCAT
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_DG_CAT
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_SMC_CAT
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_ECAT_CAT
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_DG_FUNCT
20:18:58 Presenting theory CZH_Elementary_Categories.CZH_SMC_FUNCT
20:18:59 Presenting theory CZH_Elementary_Categories.CZH_ECAT_FUNCT
20:18:59 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Hom
20:18:59 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Yoneda
20:18:59 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Order
20:18:59 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Small_Order
20:18:59 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Ordinal
20:18:59 Presenting theory CZH_Elementary_Categories.CZH_ECAT_CSimplicial
20:18:59 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Structure_Example
20:19:00 Presenting theory CZH_Elementary_Categories.CZH_ECAT_Conclusions
20:19:01 Presenting CZH_Universal_Constructions ...
20:19:01 Presenting document CZH_Universal_Constructions/document
20:19:01 Presenting document CZH_Universal_Constructions/outline
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_Introduction
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_Universal
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_Limit
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_Complete
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_Adjoints
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_Kan
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_PWKan
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_PWKan_Example
20:19:01 Presenting theory CZH_Universal_Constructions.CZH_UCAT_Conclusions
20:19:03 Presenting SpecCheck ...
20:19:03 Presenting document SpecCheck/document
20:19:03 Presenting document SpecCheck/outline
20:19:03 Presenting theory SpecCheck.SpecCheck_Base
20:19:03 Presenting theory SpecCheck.SpecCheck_Generators
20:19:03 Presenting theory SpecCheck.SpecCheck_Show
20:19:03 Presenting theory SpecCheck.SpecCheck_Output_Style
20:19:03 Presenting theory SpecCheck.SpecCheck_Shrink
20:19:03 Presenting theory SpecCheck.SpecCheck
20:19:03 Presenting theory SpecCheck.SpecCheck_Dynamic
20:19:03 Presenting theory SpecCheck.SpecCheck_Examples
20:19:03 Presenting file "util.ML"
20:19:03 Presenting file "speccheck_base.ML"
20:19:03 Presenting file "property.ML"
20:19:03 Presenting file "configuration.ML"
20:19:03 Presenting file "random.ML"
20:19:03 Presenting file "show_types.ML"
20:19:03 Presenting file "show_base.ML"
20:19:03 Presenting file "show_term.ML"
20:19:03 Presenting file "show.ML"
20:19:03 Presenting file "output_style_types.ML"
20:19:03 Presenting file "output_style_perl.ML"
20:19:03 Presenting file "output_style_custom.ML"
20:19:03 Presenting file "output_style.ML"
20:19:03 Presenting file "shrink_types.ML"
20:19:03 Presenting file "shrink_base.ML"
20:19:03 Presenting file "shrink.ML"
20:19:03 Presenting file "dynamic_construct.ML"
20:19:03 Presenting file "speccheck_dynamic.ML"
20:19:03 Presenting file "lecker.ML"
20:19:03 Presenting file "speccheck.ML"
20:19:03 Presenting file "gen_types.ML"
20:19:03 Presenting file "gen_base.ML"
20:19:03 Presenting file "gen_text.ML"
20:19:03 Presenting file "gen_int.ML"
20:19:03 Presenting file "gen_real.ML"
20:19:03 Presenting file "gen_function.ML"
20:19:03 Presenting file "gen_term.ML"
20:19:03 Presenting file "gen.ML"
20:19:03 Presenting Recursion-Addition ...
20:19:03 Presenting document Recursion-Addition/document
20:19:03 Presenting document Recursion-Addition/outline
20:19:03 Presenting theory Recursion-Addition.recursion
20:19:04 Presenting Delta_System_Lemma ...
20:19:04 Presenting document Delta_System_Lemma/document
20:19:04 Presenting document Delta_System_Lemma/outline
20:19:04 Presenting theory Delta_System_Lemma.ZF_Library
20:19:04 Presenting theory Delta_System_Lemma.Cofinality
20:19:04 Presenting theory Delta_System_Lemma.Cardinal_Library
20:19:04 Presenting theory Delta_System_Lemma.Konig
20:19:04 Presenting theory Delta_System_Lemma.Delta_System
20:19:04 Presenting theory Delta_System_Lemma.Cohen_Posets
20:19:04 Presenting Forcing ...
20:19:04 Presenting document Forcing/document
20:19:04 Presenting document Forcing/outline
20:19:04 Presenting theory Forcing.Utils
20:19:04 Presenting theory Forcing.Forcing_Notions
20:19:04 Presenting theory Forcing.Pointed_DC
20:19:04 Presenting theory Forcing.Rasiowa_Sikorski
20:19:04 Presenting theory Forcing.Nat_Miscellanea
20:19:04 Presenting theory Forcing.Internalizations
20:19:04 Presenting theory Forcing.Recursion_Thms
20:19:04 Presenting theory Forcing.Relative_Univ
20:19:04 Presenting theory Forcing.Synthetic_Definition
20:19:04 Presenting theory Forcing.Interface
20:19:04 Presenting theory Forcing.Forcing_Data
20:19:04 Presenting file "utils.ML"
20:19:04 Presenting theory Forcing.Internal_ZFC_Axioms
20:19:04 Presenting theory Forcing.Renaming
20:19:04 Presenting theory Forcing.Renaming_Auto
20:19:04 Presenting theory Forcing.Names
20:19:04 Presenting theory Forcing.FrecR
20:19:04 Presenting theory Forcing.Arities
20:19:05 Presenting theory Forcing.Forces_Definition
20:19:05 Presenting theory Forcing.Forcing_Theorems
20:19:05 Presenting theory Forcing.Separation_Rename
20:19:05 Presenting file "renaming.ML"
20:19:05 Presenting theory Forcing.Separation_Axiom
20:19:05 Presenting theory Forcing.Pairing_Axiom
20:19:05 Presenting theory Forcing.Union_Axiom
20:19:05 Presenting theory Forcing.Powerset_Axiom
20:19:05 Presenting theory Forcing.Extensionality_Axiom
20:19:05 Presenting theory Forcing.Foundation_Axiom
20:19:05 Presenting theory Forcing.Least
20:19:05 Presenting theory Forcing.Replacement_Axiom
20:19:05 Presenting theory Forcing.Infinity_Axiom
20:19:05 Presenting theory Forcing.Choice_Axiom
20:19:05 Presenting theory Forcing.Ordinals_In_MG
20:19:05 Presenting theory Forcing.Proper_Extension
20:19:05 Presenting theory Forcing.Succession_Poset
20:19:05 Presenting theory Forcing.Forcing_Main
20:19:06 
20:19:06 === TIMING ===
20:19:06 
20:19:06 Group AFP: 22:15:37 elapsed time, 62:33:09 cpu time, factor 2.81
20:19:06 Group main: 0:41:46 elapsed time, 2:09:10 cpu time, factor 3.09
20:19:06 Group timing: 0:44:01 elapsed time, 2:15:10 cpu time, factor 3.07
20:19:06 Group large: 1:03:18 elapsed time, 3:57:21 cpu time, factor 3.75
20:19:06 Overall: 3:05:55 elapsed time, 65:09:12 cpu time, factor 21.03
20:19:06 
20:19:06 === DEPENDENCIES ===
20:19:06 
20:19:06 Generating dependencies file ...
20:19:12 Writing dependencies file ...
20:19:12 
20:19:12 === COMPLETED ===
20:19:12 
20:19:12 Started calculate disk usage of build
20:19:12 Finished Calculation of disk usage of build in 0 seconds
20:19:12 Started calculate disk usage of workspace
20:19:13 Finished Calculation of disk usage of workspace in 0 seconds
20:19:13 Finished: SUCCESS