session "StarForth" = "HOL-Library" +
  description "Formal proofs of StarForth FORTH-79 primitive correctness and physics-loop invariants"
  theories [document = false]
    StarForth_Base
    StarForth_Q48_16
    StarForth_Stack_Words
    StarForth_Double_Words
    StarForth_Arithmetic_Words
    StarForth_Mixed_Arithmetic_Words
    StarForth_Logical_Words
    StarForth_Return_Stack_Words
    StarForth_Memory_Words
    StarForth_Dictionary_Words
    StarForth_Dictionary_Manipulation_Words
    StarForth_Defining_Words
    StarForth_Control_Words
    StarForth_String_Words
    StarForth_Block_Words
    StarForth_IO_Words
    StarForth_Editor_Words
    StarForth_Format_Words
    StarForth_System_Words
    StarForth_Vocabulary_Words
    StarForth_Mutex
    StarForth_Transition
    StarForth_Dictionary_Heat_Diagnostic_Words
    StarForth_Physics_Freeze_Words
    StarForth_Physics_Diagnostic_Words
    StarForth_Physics_Benchmark_Words
    StarForth_Physics_Pipelining_Diagnostic_Words
    StarForth_StarForth_Words
    StarForth_Framebuffer_Words
    StarForth_Keyboard_Words
    StarForth_Scroll_Words
    StarForth_TTF_Words
    StarForth_Lifecycle_Words_Hosted
    StarForth_Defer_Words
    StarForth_Log_Words
    StarForth_Q48_Words
    StarForth_Inference_Words
    StarForth_Loop1_Heat
    StarForth_Loop2_Window
    StarForth_Loop3_Decay
    StarForth_Loop4_Pipeline
    StarForth_Loop5_WinInf
    StarForth_Loop6_DecayInf
    StarForth_Loop7_Heartrate
    StarForth_Concurrent
    StarForth_Correctness
    ACL_Pin_Monotone
    ACL_Inherit_Clears_Pin
    ACL_TTL_Bounded
    ACL_Emergency_Bypass
    ACL_No_Escalation
    StarForth_ACL_Words