summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHannes Schulze <haschu0103@outlook.de>2025-10-22 23:30:39 +0200
committerHannes Schulze <haschu0103@outlook.de>2025-10-22 23:30:39 +0200
commitb1a5137ed3f2d7810a1670d2e3888e8a87d89b02 (patch)
treeb9b0a5a6c225ee3d85f1b5f2d33c8c222161964f
parent32f51048343ee23e6382e5aff37308ec015fcdf3 (diff)
update imports
-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