From 49c008ef405ab8d8229ae1d5b0737339ee46e576 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 17 Sep 2018 16:00:56 +0200 Subject: Clean up Equal.thy + some other tweaks --- HoTT_Base.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'HoTT_Base.thy') diff --git a/HoTT_Base.thy b/HoTT_Base.thy index efc6182..17e3142 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -77,7 +77,7 @@ Declare named theorems to be used by proof methods defined in @{file HoTT_Method These are used by the \compute\ method, and may also be passed to invocations of the method \subst\ to perform equational rewriting. \ -(* Todo: Set up the simplifier! *) +(* Todo: Set up the Simplifier! *) end -- cgit v1.2.3