Commit c5fc806e authored by wenzelm's avatar wenzelm
Browse files

maintain individual ROOT in each subdirectory, with central copy produced via isabelle afp_mkroot;

parent cbdeae1ecb24
session "AVL-Trees"! (AFP) in "." = HOL +
theories
AVL
AVL2
files
"document/root.tex"
session Abortable_Linearizable_Modules! (AFP) in "." = HOLCF +
theories [document = false]
"~~/src/HOL/Library/List_Prefix"
"~~/src/HOL/HOLCF/IOA/meta_theory/IOA"
theories
CompositionCorrectness
files
"document/abstract.tex"
"document/introduction.tex"
"document/root.bib"
"document/root.tex"
session "Abstract-Hoare-Logics"! (AFP) in "." = HOL +
theories
"While/HoareTotal"
"Proc/PHoareTotal"
"Procs/PsHoareTotal"
files
"document/root.bib"
"document/root.tex"
session "Abstract-Rewriting"! (AFP) in "." = HOL +
theories [document = false]
"../Transitive-Closure/Transitive_Closure_Impl"
"../Regular-Sets/Regexp_Method"
theories
Seq
Abstract_Rewriting
Relative_Rewriting
SN_Orders
SN_Order_Carrier
files
"document/root.bib"
"document/root.tex"
session ArrowImpossibilityGS! (AFP) in "." = HOL +
theories [document = false]
"~~/src/HOL/Library/FuncSet"
"~~/src/HOL/Library/Zorn"
theories
"Thys/Arrow_Utility"
"Thys/GS"
files
"document/root.bib"
"document/root.tex"
session "AutoFocus-Stream"! (AFP) in "." = "Nat-Interval-Logic" +
options [document_graph]
theories
ListSlice
AF_Stream
AF_Stream_Exec
IL_AF_Stream
IL_AF_Stream_Exec
files
"document/root.tex"
session BDD! (AFP) in "." = Simpl +
options [document_graph]
theories
EvalProof
NormalizeTotalProof
files
"document/root.bib"
"document/root.tex"
session BinarySearchTree! (AFP) in "." = HOL +
theories
BinaryTree
BinaryTree_Map
BinaryTree_TacticStyle
files
"document/root.tex"
session "Binomial-Heaps"! (AFP) in "." = HOL +
theories [document = false]
"~~/src/HOL/Library/Multiset"
theories
BinomialHeap
SkewBinomialHeap
theories [document = false]
"~~/src/HOL/Library/Efficient_Nat"
theories [document = false]
Test
(* FIXME *)
(* Keep these in, they are to early detect problems with the code generator *)
files
"document/root.bib"
"document/root.tex"
session "Binomial-Queues"! (AFP) in "." = HOL +
theories
PQ_Implementation
files
"document/haftmann.sty"
"document/llncs.cls"
"document/root.tex"
session BytecodeLogicJmlTypes! (AFP) in "." = HOL +
theories
Sound
Cachera
files
"document/root.bib"
"document/root.tex"
session Category! (AFP) in "." = HOL +
theories [document = false]
"~~/src/HOL/Library/FuncSet"
theories
Cat
SetCat
Functors
HomFunctors
NatTrans
Yoneda
(* FIXME *)
(*License: LGPL
All files in this development of Category Theory are licensed under LGPL.*)
files
"document/root.bib"
"document/root.tex"
session Category2! (AFP) in "." = HOL +
theories [document = false]
"~~/src/HOL/Library/FuncSet"
"~~/src/HOL/Library/Multiset"
"~~/src/HOL/ZF/MainZF"
theories
MonadicEquationalTheory
Yoneda
files
"document/root.bib"
"document/root.tex"
session Cauchy! (AFP) in "." = HOL +
theories [show_question_marks = false]
CauchysMeanTheorem
CauchySchwarz
files
"document/root.tex"
session Circus! (AFP) in "." = HOLCF +
options [document_graph]
theories [document = false]
"~~/src/HOL/Library/List_Prefix"
theories
Refinement_Example
files
"document/acronym.sty"
"document/bigfoot.sty"
"document/circus.sty"
"document/comment.sty"
"document/csp.sty"
"document/fixme.sty"
"document/fmde-acronyms.sty"
"document/hol-ocl-isar.sty"
"document/lstisar-mbt.sty"
"document/marginnote.sty"
"document/perpage.sty"
"document/proof.sty"
"document/prooftree.sty"
"document/root.bib"
"document/root.tex"
"document/suffix.sty"
"document/xcolor.sty"
"document/zed.sty"
session ClockSynchInst! (AFP) in "." = HOL +
theories
ICAInstance
LynchInstance
(* FIXME *)
(* Title: Instances of Schneider's generalized protocol of clock synchronization
Author: Damián Barsotti <damian@hal.famaf.unc.edu.ar>, 2006
Maintainer: Damián Barsotti <damian@hal.famaf.unc.edu.ar>
*)
files
"document/abs_distrib_mult.cvc"
"document/abs_distrib_mult.ics"
"document/abs_distrib_mult2.cvc"
"document/accur_pres.cvc"
"document/accur_pres.ics"
"document/bound_prec_enh.cvc"
"document/bound_prec_enh.ics"
"document/bound_prec_enh4.cvc"
"document/bound_prec_enh7.cvc"
"document/root.bib"
"document/root.tex"
session CofGroups! (AFP) in "." = HOL +
theories [document = false]
"~~/src/HOL/Library/Nat_Bijection"
theories
CofGroups
files
"document/root.bib"
"document/root.tex"
session Coinductive! (AFP) in "." = HOL +
options [document_graph]
theories [document = false]
"~~/src/HOL/Library/Extended_Nat"
"~~/src/HOL/Library/List_Prefix"
"~~/src/HOL/Library/Quotient_Syntax"
"~~/src/HOL/Library/Quotient_Product"
"~~/src/HOL/Library/Quotient_Set"
"~~/src/HOL/Library/Quotient_Sum"
"~~/src/HOL/Library/Infinite_Set"
theories
Coinductive
Lazy_TLList
files
"document/root.tex"
session Collections! (AFP) in "." = HOL +
options [document_variants = "outline=/proof,/ML:userguide"]
theories [document = false]
"common/Misc"
"common/Assoc_List"
"common/RBT_add"
"common/Dlist_add"
"common/Array"
"~~/src/HOL/Library/Efficient_Nat"
"~~/src/HOL/Library/While_Combinator"
"../Binomial-Heaps/BinomialHeap"
"../Binomial-Heaps/SkewBinomialHeap"
"../Finger-Trees/FingerTree"
theories
"spec/Spec_Chapter"
"spec/MapSpec"
"spec/SetSpec"
"spec/ListSpec"
"spec/AnnotatedListSpec"
"spec/PrioSpec"
"spec/PrioUniqueSpec"
"gen_algo/Gen_Algo_Chapter"
"gen_algo/MapGA"
"gen_algo/SetGA"
"gen_algo/SetByMap"
"gen_algo/ListGA"
"gen_algo/SetIndex"
"gen_algo/Algos"
"gen_algo/PrioByAnnotatedList"
"gen_algo/PrioUniqueByAnnotatedList"
"impl/Impl_Chapter"
"impl/Impl_Overview"
"impl/MapStdImpl"
"impl/SetStdImpl"
"impl/Fifo"
"impl/BinoPrioImpl"
"impl/SkewPrioImpl"
"impl/FTAnnotatedListImpl"
"impl/FTPrioImpl"
"impl/FTPrioUniqueImpl"
theories [document = false]
"gen_algo/StdInst"
theories
Collections
Userguide
"examples/Examples_Chapter"
"examples/itp_2010"
"examples/Exploration"
"examples/Exploration_DFS"
"examples/All"
(* FIXME *)
(* Specifications *)
(* Generic Algorithms *)
(* Implementations *)
(* Examples *)
files
"document/conclusion.tex"
"document/documentation.tex"
"document/intro.tex"
"document/root.bib"
"document/root.tex"
"document/root_userguide.bib"
"document/root_userguide.tex"
session "Compiling-Exceptions-Correctly"! (AFP) in "." = HOL +
theories
Exceptions
files
"document/root.bib"
"document/root.tex"
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment