From 68aa069172933b875d70a5ef71e9db0ae685a92d Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 17 Feb 2019 18:34:38 +0100
Subject: Method "quantify" converts product inhabitation into Pure universal
 statements. Also misc. cleanups.

---
 Projections.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Projections.thy')

diff --git a/Projections.thy b/Projections.thy
index c819240..8ff6b30 100644
--- a/Projections.thy
+++ b/Projections.thy
@@ -39,7 +39,7 @@ lemma snd_cmp:
   assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "snd A B <a,b> \<equiv> b"
 unfolding snd_def by (derive lems: assms)
 
-lemmas Proj_types [intro] = fst_type snd_type
-lemmas Proj_comps [comp] = fst_cmp snd_cmp
+lemmas Proj_type [intro] = fst_type snd_type
+lemmas Proj_comp [comp] = fst_cmp snd_cmp
 
 end
-- 
cgit v1.2.3