Session JinjaThreads
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Sublist
HOL-Library.Transitive_Closure_Table
HOL-Library.Predicate_Compile_Alternative_Defs
HOL-Library.Confluence
HOL-Library.Confluent_Quotient
HOL-Library.Dlist
Set_without_equal
HOL-Library.Adhoc_Overloading
File ‹adhoc_overloading.ML›
HOL-Library.Monad_Syntax
Set_Monad
HOL-Library.Infinite_Set
HOL-Library.Case_Converter
File ‹case_converter.ML›
HOL-Library.Simps_Case_Conv
File ‹simps_case_conv.ML›
HOL-Library.Old_Datatype
File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
HOL-Library.Nat_Bijection
HOL-Library.Countable
File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
HOL-Library.Countable_Set
HOL-Library.Countable_Complete_Lattices
HOL-Library.Order_Continuity
HOL-Library.Extended_Nat
HOL-Library.Complete_Partial_Order2
Coinductive.Coinductive_Nat
Coinductive.Coinductive_List
Coinductive.TLList
Coinductive.Lazy_LList
Coinductive.Lazy_TLList
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
HOL-ex.Quicksort
HOL-Library.Option_ord
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
Automatic_Refinement.Misc
Automatic_Refinement.Foldi
Collections.SetIterator
Collections.SetIteratorOperations
Automatic_Refinement.Refine_Util_Bootstrap1
Automatic_Refinement.Mpat_Antiquot
Automatic_Refinement.Mk_Term_Antiquot
Automatic_Refinement.Refine_Util
Automatic_Refinement.Attr_Comb
Automatic_Refinement.Named_Sorted_Thms
Automatic_Refinement.Prio_List
Automatic_Refinement.Tagged_Solver
Automatic_Refinement.Anti_Unification
Automatic_Refinement.Indep_Vars
Automatic_Refinement.Select_Solve
Automatic_Refinement.Mk_Record_Simp
Automatic_Refinement.Refine_Lib
File ‹Cond_Rewr_Conv.ML›
File ‹Revert_Abbrev.ML›
Collections.Proper_Iterator
Collections.It_to_It
Collections.SetIteratorGA
Refine_Monadic.Refine_Chapter
Automatic_Refinement.Autoref_Phases
Automatic_Refinement.Autoref_Data
Automatic_Refinement.Autoref_Tagging
Automatic_Refinement.Relators
Automatic_Refinement.Param_Tool
Automatic_Refinement.Param_HOL
Automatic_Refinement.Parametricity
Automatic_Refinement.Autoref_Id_Ops
Automatic_Refinement.Autoref_Fix_Rel
Automatic_Refinement.Autoref_Translate
Automatic_Refinement.Autoref_Gen_Algo
Automatic_Refinement.Autoref_Relator_Interface
Automatic_Refinement.Autoref_Tool
Automatic_Refinement.Autoref_Bindings_HOL
Automatic_Refinement.Automatic_Refinement
Refine_Monadic.Refine_Mono_Prover
File ‹refine_mono_prover.ML›
Refine_Monadic.Refine_Misc
Refine_Monadic.RefineG_Transfer
Refine_Monadic.RefineG_Domain
Refine_Monadic.RefineG_Recursion
Refine_Monadic.RefineG_Assert
Refine_Monadic.Refine_Basic
Refine_Monadic.Refine_Leof
Refine_Monadic.Refine_Heuristics
Refine_Monadic.Refine_More_Comb
HOL-Library.While_Combinator
Refine_Monadic.RefineG_While
Refine_Monadic.Refine_While
Refine_Monadic.Refine_Det
Refine_Monadic.Refine_Pfun
Refine_Monadic.Refine_Transfer
Refine_Monadic.Refine_Foreach
Refine_Monadic.Refine_Automation
Refine_Monadic.Autoref_Monadic
Refine_Monadic.Refine_Monadic
Collections.Gen_Iterator
Collections.Idx_Iterator
Collections.Iterator
Collections.ICF_Tools
Collections.Ord_Code_Preproc
Collections.Record_Intf
Collections.Locale_Code
Collections.ICF_Spec_Base
Collections.SetSpec
Collections.MapSpec
Collections.ListSpec
Collections.AnnotatedListSpec
Collections.PrioSpec
Collections.PrioUniqueSpec
Collections.Algos
Collections.SetIndex
Collections.SetIteratorCollectionsGA
Collections.SetGA
Collections.Dlist_add
Collections.ListSetImpl
Collections.ListSetImpl_Invar
Collections.ListSetImpl_NotDist
Collections.Sorted_List_Operations
Collections.ListSetImpl_Sorted
HOL-Library.RBT_Impl
Collections.RBT_add
HOL-Library.RBT
Collections.MapGA
Collections.RBTMapImpl
Collections.SetByMap
Collections.RBTSetImpl
HOL-Library.AList
Collections.Assoc_List
Collections.ListMapImpl
HOL-Library.Phantom_Type
HOL-Library.Cardinality
HOL-Library.Numeral_Type
HOL-Library.Type_Length
HOL-Library.Word
File ‹Tools/word_lib.ML›
File ‹Tools/smt_word.ML›
Word_Lib.More_Arithmetic
Word_Lib.More_Divides
Word_Lib.More_Bit_Ring
Word_Lib.More_Word
Word_Lib.Bit_Shifts_Infix_Syntax
Word_Lib.Most_significant_bit
Word_Lib.Least_significant_bit
Word_Lib.Generic_set_bit
Word_Lib.Bit_Comprehension
HOL-Library.Signed_Division
Word_Lib.Signed_Division_Word
Native_Word.Code_Target_Word_Base
Native_Word.Word_Type_Copies
Native_Word.Code_Int_Integer_Conversion
Native_Word.Code_Target_Integer_Bit
Native_Word.Uint32
Collections.HashCode
HOL-Library.Code_Target_Int
HOL-Library.Code_Abstract_Nat
HOL-Library.Code_Target_Nat
HOL-Library.Code_Target_Numeral
Native_Word.Code_Target_Int_Bit
Collections.Code_Target_ICF
Collections.HashMap_Impl
Collections.HashMap
Collections.HashSet
Trie.Trie
Collections.Trie_Impl
Collections.Trie2
Collections.TrieMapImpl
Collections.TrieSetImpl
Collections.Diff_Array
Collections.ListGA
Collections.Array_Iterator
Collections.ArrayHashMap_Impl
Collections.ArrayHashMap
Collections.ArrayHashSet
Collections.ArrayMapImpl
Collections.ArraySetImpl
Collections.SetStdImpl
Collections.ListMapImpl_Invar
Collections.MapStdImpl
Collections.Fifo
Binomial-Heaps.BinomialHeap
Collections.BinoPrioImpl
Binomial-Heaps.SkewBinomialHeap
Collections.SkewPrioImpl
Finger-Trees.FingerTree
Collections.FTAnnotatedListImpl
Collections.PrioByAnnotatedList
Collections.FTPrioImpl
Collections.PrioUniqueByAnnotatedList
Collections.FTPrioUniqueImpl
Collections.ICF_Impl
Collections.ICF_Refine_Monadic
Collections.Intf_Set
Collections.Intf_Map
Collections.ICF_Autoref
Collections.DatRef
Collections.Collections
Collections.CollectionsV1
JT_ICF
FinFun.FinFun
Auxiliary
Basic_Main
FWState
FWLock
FWLocking
FWThread
FWWait
FWCondAction
FWWellform
FWLockingThread
FWInterrupt
FWSemantics
FWProgressAux
FWDeadlock
FWProgress
FWLifting
LTS
FWLTS
Bisimulation
FWBisimulation
FWBisimDeadlock
FWLiftingSem
FWInitFinLift
FWBisimLift
Semilat
Err
Opt
Product
Listn
Semilattices
Typing_Framework
SemilatAlg
Typing_Framework_err
Kildall
LBVSpec
LBVCorrect
LBVComplete
Abstract_BV
Type
Decl
TypeRel
Value
Exceptions
SystemClasses
Heap
Observable_Events
StartConfig
Conform
ExternalCall
WellForm
ExternalCallWF
ConformThreaded
BinOp
SemiType
Common_Main
State
Expr
JHeap
SmallStep
WWellForm
WellType
DefAss
JWellForm
Threaded
WellTypeRT
Progress
DefAssPreservation
TypeSafe
ProgressThreaded
Deadlocked
Annotate
J_Main
JVMState
JVMInstructions
JVMHeap
JVMExecInstr
JVMExceptions
JVMExec
JVMDefensive
JVMThreaded
JVM_Main
JVM_SemiType
Effect
BVSpec
BVConform
BVSpecTypeSafe
BVNoTypeError
BVProgressThreaded
JVMDeadlocked
EffectMono
TF_JVM
LBVJVM
BVExec
BCVExec
BV_Main
CallExpr
J0
J0Bisim
J1State
J1Heap
J1
J1Deadlock
PCompiler
Compiler2
Exception_Tables
J1WellType
J1WellForm
HOL-Library.Prefix_Order
TypeComp
JVMTau
Execs
J1JVMBisim
J1JVM
JVMJ1
Correctness2
ListIndex
Compiler1
J0J1Bisim
Correctness1Threaded
Correctness1
JJ1WellForm
Compiler
Correctness
Preprocessor
Compiler_Main
MM
SC
SC_Interp
SC_Collections
Orders
JMM_Spec
JMM_DRF
SC_Legal
Non_Speculative
SC_Completion
HB_Completion
JMM_Heap
JMM_Framework
JMM_Typesafe
JMM_Common
JMM_J
DRF_J
JMM_JVM
DRF_JVM
JMM_Type
JMM_Compiler
JMM_Type2
JMM_Interp
JMM_Typesafe2
JMM_J_Typesafe
JMM_JVM_Typesafe
JMM_Compiler_Type2
JMM
MM_Main
State_Refinement
Scheduler
Random_Scheduler
Round_Robin
SC_Schedulers
HOL-Library.Mapping
HOL-Library.AList_Mapping
TypeRelRefine
PCompilerRefine
J_Execute
ExternalCall_Execute
JVMExec_Execute2
JVM_Execute2
HOL-Library.Code_Cardinality
Code_Generation
JVMExec_Execute
JVM_Execute
ToString
Java2Jinja
Execute_Main
ApprenticeChallenge
BufferExample
Examples_Main
JinjaThreads