Session Isabelle_LLVM_Time

Theories

• Named_Simpsets
  • File ‹named_simpsets.ML›
• Misc_LLang
• More_List
• More_Eisbach_Tools
• Find_In_Thms
• Basic_Imports
• Lenses
• ELenses
• Monad
• Sep_Value
• Sep_Block_Allocator
• Sep_Array_Block
• Bits_Natural
• LLVM_More_Word
• LLVM_Integer
• LLVM_Memory
• Abstract_Cost
• LLVM_Shallow
• LLVM_Codegen
  • File ‹LLVM_Builder.ml›
• Monadify
• Definition_Utils
• LLVM_Codegen_Preproc
• LLVM_Basic_Main
• Sep_Algebra_Add
• Defer_Slot
• Basic_VCG
  • File ‹subgoal_focus_some.ML›
• Frame_Infer
• Enat_Cost
• Sep_Generic_Wp
• Sep_Lift
• Sep_Value_RS
• Sep_Block_Allocator_RS
• Sep_Array_Block_RS
• LLVM_Memory_RS
• LLVM_Shallow_RS
• LLVM_VCG_Main
• LLVM_DS_Arith
• LLVM_DS_Array
• LLVM_DS_NArray
• PO_Normalizer
  • File ‹PO_Normalizer.ML›
• Sepref_Misc
• Structured_Apply
• NREST_Misc
• NREST
• NREST_Type_Classes
• Time_Refinement
• Data_Refinement
• NREST_Backwards_Reasoning
• NREST_Automation
• NREST_Main
• Sepref_Id_Op
• More_Refine_Util
• Sepref_Basic
• Sepref_Monadify
• Sepref_Constraints
• Sepref_Frame
• Sepref_Rules
• Sepref_Combinator_Setup
• User_Smashing
• Sepref_Translate
• Term_Synth
• Sepref_Definition
• Concl_Pres_Clarification
• Sepref_Intf_Util
• Sepref_Tool
• Sepref_HOL_Bindings
• Sepref
• Proto_EOArray
• LLVM_DS_Dflt
• Hnr_Primitives_Experiment
• Sorting_Misc
• Refine_Heuristics
• Sorting_Setup
• Sorting_Partially_Sorted
• Sorting_Quicksort_Scheme
• Sorting_Unguarded_Insertion_Sort
• Sorting_Final_insertion_Sort
• Asymptotics_1D
  • File ‹landau_util.ML›
  • File ‹master_theorem_wrapper.ML›
• Asymptotics_2D
  • File ‹landau_util_2d.ML›
• More_Asymptotics
• Sorting_Heapsort
• Sorting_Log2
• Sorting_Quicksort_Partition
• Sorting_Introsort
• Currs_Of
• Synth_Rate
• Dynamic_Array
• Sorting_Strings
• Sorting_Export_Code
• Sorting_Results