summaryrefslogtreecommitdiff
path: root/Nominal
diff options
context:
space:
mode:
Diffstat (limited to 'Nominal')
-rw-r--r--Nominal/Instances.lean2
-rw-r--r--Nominal/Permutations.lean2
-rw-r--r--Nominal/Support.lean2
3 files changed, 3 insertions, 3 deletions
diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
index decc0cb..057a0de 100644
--- a/Nominal/Instances.lean
+++ b/Nominal/Instances.lean
@@ -1,6 +1,6 @@
+import Mathlib
import Nominal.Permutations
import Nominal.Support
-import Mathlib
/-!
# Instances
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 6819c67..dd9b9d2 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -1,4 +1,4 @@
-import Mathlib.Tactic
+import Mathlib
/-!
# Finitely supported permutations
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 0df541c..efed617 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -1,4 +1,4 @@
-import Mathlib.Tactic
+import Mathlib
import Nominal.Permutations
import Nominal.Helpers.Finset