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
73b6fa45e1bb
Commit
519f4008
authored
Nov 03, 2014
by
wenzelm
Browse files
modernized header uniformly as section;
parent
33c3c1e98475
Changes
825
Hide whitespace changes
Inline
Side-by-side
thys/AVL-Trees/AVL.thy
View file @
73b6fa45
...
...
@@ -8,7 +8,7 @@
see the file Changelog for a list of changes
*)
header
"AVL Trees"
section
"AVL Trees"
theory AVL
imports Main
...
...
thys/AVL-Trees/AVL2.thy
View file @
73b6fa45
...
...
@@ -8,7 +8,7 @@
see the file Changelog for a list of changes
*)
header
{* AVL Trees in 2 Stages *}
section
{* AVL Trees in 2 Stages *}
theory AVL2
imports Main
...
...
thys/AWN/AWN.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Terms of the Algebra for Wireless Networks"
section
"Terms of the Algebra for Wireless Networks"
theory AWN
imports Lib
...
...
thys/AWN/AWN_Cterms.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Control terms and well-definedness of sequential processes"
section
"Control terms and well-definedness of sequential processes"
theory AWN_Cterms
imports AWN
...
...
thys/AWN/AWN_Invariants.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Generic invariants on sequential AWN processes"
section
"Generic invariants on sequential AWN processes"
theory AWN_Invariants
imports Invariants AWN_SOS AWN_Labels
...
...
thys/AWN/AWN_Labels.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Labelling sequential processes"
section
"Labelling sequential processes"
theory AWN_Labels
imports AWN AWN_Cterms
...
...
thys/AWN/AWN_Main.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Import all AWN-related theories"
section
"Import all AWN-related theories"
theory AWN_Main
imports AWN_SOS AWN_SOS_Labels OAWN_SOS_Labels AWN_Invariants
...
...
thys/AWN/AWN_SOS.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Semantics of the Algebra of Wireless Networks"
section
"Semantics of the Algebra of Wireless Networks"
theory AWN_SOS
imports TransitionSystems AWN
...
...
thys/AWN/AWN_SOS_Labels.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Configure the inv-cterms tactic for sequential processes"
section
"Configure the inv-cterms tactic for sequential processes"
theory AWN_SOS_Labels
imports AWN_SOS Inv_Cterms
...
...
thys/AWN/Closed.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Lemmas for closed networks"
section
"Lemmas for closed networks"
theory Closed
imports Pnet
...
...
thys/AWN/Inv_Cterms.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"A custom tactic for showing invariants via control terms"
section
"A custom tactic for showing invariants via control terms"
theory Inv_Cterms
imports AWN_Labels
...
...
thys/AWN/Invariants.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Reachability and Invariance"
section
"Reachability and Invariance"
theory Invariants
imports Lib TransitionSystems
...
...
thys/AWN/Lib.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Generic functions and lemmas"
section
"Generic functions and lemmas"
theory Lib
imports Main
...
...
thys/AWN/OAWN_Convert.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Transfer standard invariants into open invariants"
section
"Transfer standard invariants into open invariants"
theory OAWN_Convert
imports AWN_SOS_Labels AWN_Invariants
...
...
thys/AWN/OAWN_Invariants.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Generic open invariants on sequential AWN processes"
section
"Generic open invariants on sequential AWN processes"
theory OAWN_Invariants
imports Invariants OInvariants
...
...
thys/AWN/OAWN_SOS.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Open semantics of the Algebra of Wireless Networks"
section
"Open semantics of the Algebra of Wireless Networks"
theory OAWN_SOS
imports TransitionSystems AWN
...
...
thys/AWN/OAWN_SOS_Labels.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Configure the inv-cterms tactic for open sequential processes"
section
"Configure the inv-cterms tactic for open sequential processes"
theory OAWN_SOS_Labels
imports OAWN_SOS Inv_Cterms
...
...
thys/AWN/OClosed_Lifting.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Lifting rules for (open) closed networks"
section
"Lifting rules for (open) closed networks"
theory OClosed_Lifting
imports OPnet_Lifting
...
...
thys/AWN/OClosed_Transfer.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Transfer open results onto closed models"
section
"Transfer open results onto closed models"
theory OClosed_Transfer
imports Closed OClosed_Lifting
...
...
thys/AWN/OInvariants.thy
View file @
73b6fa45
...
...
@@ -3,7 +3,7 @@
Author: Timothy Bourke
*)
header
"Open reachability and invariance"
section
"Open reachability and invariance"
theory OInvariants
imports Invariants
...
...
Prev
1
2
3
4
5
…
42
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