Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
24c883709f93
Commit
9c4746a0
authored
Apr 29, 2014
by
wenzelm
Browse files
systematic replacement of 'files' by 'document_files';
parent
ede7dddb16d0
Changes
167
Hide whitespace changes
Inline
Side-by-side
thys/AVL-Trees/ROOT
View file @
24c88370
...
...
@@ -5,5 +5,5 @@ session "AVL-Trees" (AFP) = HOL +
theories
AVL
AVL2
files
"
document/
root.tex"
document_
files
"root.tex"
thys/AWN/ROOT
View file @
24c88370
...
...
@@ -32,7 +32,7 @@ session AWN (AFP) = HOL +
AWN_Main
Toy
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/Abortable_Linearizable_Modules/ROOT
View file @
24c88370
...
...
@@ -7,8 +7,8 @@ session Abortable_Linearizable_Modules (AFP) = HOLCF +
"~~/src/HOL/HOLCF/IOA/meta_theory/IOA"
theories
CompositionCorrectness
files
"
document/
abstract.tex"
"
document/
introduction.tex"
"
document/
root.bib"
"
document/
root.tex"
document_
files
"abstract.tex"
"introduction.tex"
"root.bib"
"root.tex"
thys/Abstract-Hoare-Logics/ROOT
View file @
24c88370
...
...
@@ -6,6 +6,6 @@ session "Abstract-Hoare-Logics" (AFP) = HOL +
"While/HoareTotal"
"Proc/PHoareTotal"
"Procs/PsHoareTotal"
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/Abstract-Rewriting/ROOT
View file @
24c88370
...
...
@@ -11,6 +11,6 @@ session "Abstract-Rewriting" (AFP) = HOL +
Relative_Rewriting
SN_Orders
SN_Order_Carrier
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/Abstract_Completeness/ROOT
View file @
24c88370
...
...
@@ -9,6 +9,6 @@ session Abstract_Completeness (AFP) = "HOL" +
theories
Abstract_Completeness
Propositional_Logic
files
"
document/
root.tex"
"
document/
root.bib"
document_
files
"root.tex"
"root.bib"
thys/Affine_Arithmetic/ROOT
View file @
24c88370
...
...
@@ -8,6 +8,6 @@ session Affine_Arithmetic (AFP) = "HOL-Multivariate_Analysis" +
"~~/src/HOL/Library/Float"
theories
Affine_Arithmetic
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/ArrowImpossibilityGS/ROOT
View file @
24c88370
...
...
@@ -5,6 +5,6 @@ session ArrowImpossibilityGS (AFP) = "HOL-Library" +
theories
"Thys/Arrow_Utility"
"Thys/GS"
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/AutoFocus-Stream/ROOT
View file @
24c88370
...
...
@@ -8,5 +8,5 @@ session "AutoFocus-Stream" (AFP) = "Nat-Interval-Logic" +
AF_Stream_Exec
IL_AF_Stream
IL_AF_Stream_Exec
files
"
document/
root.tex"
document_
files
"root.tex"
thys/Automatic_Refinement/ROOT
View file @
24c88370
...
...
@@ -25,5 +25,5 @@ session Automatic_Refinement (AFP) = HOL +
"Autoref_Bindings_HOL"
"Automatic_Refinement"
files
"
document/
root.tex"
document_
files
"root.tex"
thys/BDD/ROOT
View file @
24c88370
...
...
@@ -5,6 +5,6 @@ session BDD (AFP) = Simpl +
theories
EvalProof
NormalizeTotalProof
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/BinarySearchTree/ROOT
View file @
24c88370
...
...
@@ -6,5 +6,5 @@ session BinarySearchTree (AFP) = HOL +
BinaryTree
BinaryTree_Map
BinaryTree_TacticStyle
files
"
document/
root.tex"
document_
files
"root.tex"
thys/Binomial-Heaps/ROOT
View file @
24c88370
...
...
@@ -8,6 +8,6 @@ session "Binomial-Heaps" (AFP) = "HOL-Library" +
theories [document = false]
(* Keep these in, they are to early detect problems with the code generator *)
Test
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/Binomial-Queues/ROOT
View file @
24c88370
...
...
@@ -4,7 +4,7 @@ session "Binomial-Queues" (AFP) = HOL +
options [timeout = 600]
theories
PQ_Implementation
files
"
document/
haftmann.sty"
"
document/
llncs.cls"
"
document/
root.tex"
document_
files
"haftmann.sty"
"llncs.cls"
"root.tex"
thys/Bounded_Deducibility_Security/ROOT
View file @
24c88370
...
...
@@ -4,4 +4,4 @@ session "Bounded_Deducibility_Security" (AFP) = HOL +
options [timeout = 600]
theories
Bounded_Deducibility_Security
files "
document
/
root.tex" "
document/
intro.tex"
document
_files "
root.tex" "intro.tex"
thys/BytecodeLogicJmlTypes/ROOT
View file @
24c88370
...
...
@@ -5,6 +5,6 @@ session BytecodeLogicJmlTypes (AFP) = HOL +
theories
Sound
Cachera
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/CCS/ROOT
View file @
24c88370
...
...
@@ -4,6 +4,6 @@ session CCS (AFP) = "HOL-Nominal" +
options [timeout = 600]
theories
Weak_Cong_Pres
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/Category/ROOT
View file @
24c88370
...
...
@@ -9,6 +9,6 @@ session Category (AFP) = "HOL-Library" +
HomFunctors
NatTrans
Yoneda
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/Category2/ROOT
View file @
24c88370
...
...
@@ -7,6 +7,6 @@ session Category2 (AFP) = "HOL-Library" +
theories
MonadicEquationalTheory
Yoneda
files
"
document/
root.bib"
"
document/
root.tex"
document_
files
"root.bib"
"root.tex"
thys/Cauchy/ROOT
View file @
24c88370
...
...
@@ -5,5 +5,5 @@ session Cauchy (AFP) = HOL +
theories [show_question_marks = false]
CauchysMeanTheorem
CauchySchwarz
files
"
document/
root.tex"
document_
files
"root.tex"
Prev
1
2
3
4
5
…
9
Next
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment