aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Theorems.thy
diff options
context:
space:
mode:
Diffstat (limited to 'HoTT_Theorems.thy')
-rw-r--r--HoTT_Theorems.thy1
1 files changed, 1 insertions, 0 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index 5578bf8..f05363a 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -66,6 +66,7 @@ proof
qed (rule assms)
qed (rule assms)
+(**** GOOD CANDIDATE FOR AUTOMATION - EISBACH! ****)
proposition triply_curried:
fixes
A::Term and