8000 Merge `improvement/imports-layout` of pull request #109 into `master` · input-output-hk/thorn-calculus@3051561 · GitHub
[go: up one dir, main page]
Skip to content

Commit 3051561

Browse files
jeltschjeltsch
committed
Merge improvement/imports-layout of pull request #109 into master
Improve the layout of `imports` clauses
2 parents 1edbaed + f96c4fe commit 3051561

7 files changed

+21
-20
lines changed

‎src/Thorn_Calculus-Actions.thy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
section \<open>Actions\<close>
22

33
theory "Thorn_Calculus-Actions"
4-
imports
5-
"Thorn_Calculus-Foundations"
4+
imports
5+
"Thorn_Calculus-Foundations"
66
begin
77

88
datatype io_kind =

‎src/Thorn_Calculus-Core_Bisimilarities.thy

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
theory "Thorn_Calculus-Core_Bisimilarities"
2-
imports "Thorn_Calculus-Semantics-Synchronous"
2+
imports
3+
"Thorn_Calculus-Semantics-Synchronous"
34
begin
45

56
named_theorems thorn_simps

‎src/Thorn_Calculus-Examples.thy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33
and then this theory should be removed.
44
*)
55
theory "Thorn_Calculus-Examples"
6-
imports
7-
"Thorn_Calculus-Semantics-Synchronous"
6+
imports
7+
"Thorn_Calculus-Semantics-Synchronous"
88
begin
99

1010
lemma

‎src/Thorn_Calculus-Foundations.thy

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
section \<open>Foundations\<close>
22

33
theory "Thorn_Calculus-Foundations"
4-
imports
5-
Main
6-
"ZFC_in_HOL.ZFC_Typeclasses"
7-
"HOL-Library.Stream"
4+
imports
5+
Main
6+
"ZFC_in_HOL.ZFC_Typeclasses"
7+
"HOL-Library.Stream"
88
begin
99

1010
text \<open>

‎src/Thorn_Calculus-Processes.thy

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
section \<open>Processes\<close>
22

33
theory "Thorn_Calculus-Processes"
4-
imports
5-
"Equivalence_Reasoner.Equivalence_Reasoner"
6-
"Transition_Systems.Transition_Systems-Foundations" \<comment> \<open>for the \<^const>\<open>compower\<close> notation\<close>
7-
"Thorn_Calculus-Foundations"
8-
"HOL-Library.BNF_Corec"
4+
imports
5+
"Equivalence_Reasoner.Equivalence_Reasoner"
6+
"Transition_Systems.Transition_Systems-Foundations" \<comment> \<open>for the \<^const>\<open>compower\<close> notation\<close>
7+
"Thorn_Calculus-Foundations"
8+
"HOL-Library.BNF_Corec"
99
begin
1010

1111
ML_file \<open>binder_preservation.ML\<close>

‎src/Thorn_Calculus-Semantics-Asynchronous.thy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
section \<open>Asynchronous Semantics\<close>
22

33
theory "Thorn_Calculus-Semantics-Asynchronous"
4-
imports
5-
"Thorn_Calculus-Semantics-Synchronous"
4+
imports
5+
"Thorn_Calculus-Semantics-Synchronous"
66
begin
77

88
fun asynchronous_transition :: "action \<Rightarrow> process family relation" (\<open>'(\<rightarrow>\<^sub>a\<lparr>_\<rparr>')\<close>) where

‎src/Thorn_Calculus-Semantics-Synchronous.thy

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
section \<open>Synchronous Semantics\<close>
22

33
theory "Thorn_Calculus-Semantics-Synchronous"
4-
imports
5-
"Transition_Systems.Transition_Systems-Weak_Mutation_Systems"
6-
"Thorn_Calculus-Actions"
7-
"Thorn_Calculus-Processes"
4+
imports
5+
"Transition_Systems.Transition_Systems-Weak_Mutation_Systems"
6+
"Thorn_Calculus-Actions"
7+
"Thorn_Calculus-Processes"
88
begin
99

1010
definition post_receive :: "nat \<Rightarrow> val family \<Rightarrow> (val \<Rightarrow> 'a family) \<Rightarrow> 'a family" where

0 commit comments

Comments
 (0)
0