From 096ce05cb57c101e13d308b5df7a7af2a0060bf2 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 16 Aug 2018 19:45:11 +0200 Subject: test new machine --- HoTT_Test.thy | 2 ++ 1 file changed, 2 insertions(+) (limited to 'HoTT_Test.thy') diff --git a/HoTT_Test.thy b/HoTT_Test.thy index 4c87e78..bce2f00 100644 --- a/HoTT_Test.thy +++ b/HoTT_Test.thy @@ -50,6 +50,8 @@ by (simple lems: assms) subsection \Function application\ +text "silly test" + proposition assumes "a : A" shows "(\<^bold>\x. x)`a \ a" by (simple lems: assms) text "Currying:" -- cgit v1.2.3