Quelle  ROOT

chapter AFP

session Zippy = HOL +
  description
    "Zippy - a Customisable Framework for Tree-Based Searches"
  options
    [timeout = 300]
  sessions
    ML_Unification
    SpecCheck
  directories
    "Antiquotations"
    "Gen_Lists"
    "Gen_Lists/Lists_1"
    "Gen_Zippers/"
    "Gen_Zippers/Zippers5"
    "Gen_Zippers/Zippers5/Alternating_Zippers"
    "Gen_Zippers/Zippers5/Alternating_Zippers/Instances"
    "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/Nodes"
    "Gen_Zippers/Zippers5/Alternating_Zippers/Paths"
    "Gen_Zippers/Zippers5/Alternating_Zippers/Utils"
    "Gen_Zippers/Zippers5/Linked_Zippers"
    "Gen_Zippers/Zippers5/Morphs"
    "Gen_Zippers/Zippers5/Structured_Lenses"
    "Gen_Zippers/Zippers5/Zippers"
    "Gen_Zippers/Zippers5/Zippers/Instances"
    "Gen_Zippers/Zippers5/Zippers/Utils"
    "Generic_Data"
    "ML_Typeclasses/Antiquotations"
    "ML_Typeclasses/Gen_Coroutines"
    "ML_Typeclasses/Gen_Coroutines/Coroutines_1"
    "ML_Typeclasses/Gen_Typeclasses"
    "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1"
    "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/Categories"
    "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/Lenses"
    "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/State"
    "Priority_Queues"
    "Tactics"
    "Tactics/Blast"
    "Tactics/Cases"
    "Tactics/Induction"
    "Tactics/Metis"
    "Tactics/Simp"
    "Union_Find"
    "Zippy"
    "Zippy/Action_Applications"
    "Zippy/Action_Applications/Base"
    "Zippy/Action_Clusters"
    "Zippy/Actions"
    "Zippy/Actions/Base"
    "Zippy/Actions/Positions"
    "Zippy/Base"
    "Zippy/Coroutines"
    "Zippy/Collect"
    "Zippy/Collect/Lists"
    "Zippy/Collect/Lists_Positions"
    "Zippy/Enums"
    "Zippy/Exceptions"
    "Zippy/Goal_Pos_Updates"
    "Zippy/Goal_Pos_Updates/Base"
    "Zippy/Goal_Pos_Updates/Lists"
    "Zippy/Goals"
    "Zippy/Goals/Base"
    "Zippy/Goals/Lists"
    "Zippy/Identifiers"
    "Zippy/Instances"
    "Zippy/Instances/Cases"
    "Zippy/Instances/Classical"
    "Zippy/Instances/Hom_Changed_Goals_Data"
    "Zippy/Instances/Induction"
    "Zippy/Instances/Resolves"
    "Zippy/Instances/Resolves_Simp"
    "Zippy/Instances/Simp"
    "Zippy/Instances/Subst"
    "Zippy/Instances/Zip"
    "Zippy/Instances/Zip/Examples"
    "Zippy/Lists"
    "Zippy/Loggers"
    "Zippy/Nodes"
    "Zippy/Positions"
    "Zippy/Positions/Lists"
    "Zippy/Runs"
    "Zippy/Runs/Base"
    "Zippy/Seqs"
    "Zippy/Shows"
    "Zippy/States"
    "Zippy/Tactics"
    "Zippy/Tactics/Base"
  theories
    ML_Typeclasses
    ML_ITypeclasses
    Zip_Examples
    Zippy_Paper
  document_files
    "root.tex"
    "root.bib"

session Zip_Benchmarks in "Zippy/Instances/Zip/Examples/Benchmarks" = "HOL-Data_Structures" +
  description
    "Benchmarks for zip"
  options
    [timeout = 600]
  sessions
    "HOL-Library"
    "Zippy"
  theories
    Binomial
    Deriv
    Filter
    Finite_Set
    GCD
    Limits
    List
    Set
    Tree234_Set
    Word