From 77aa10763429d2ded040071fbf7bee331dd52f5e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 31 Jul 2020 18:10:10 +0200
Subject: (REF) Tweak attribute names in preparation for new logical
 introduction rule behavior

---
 spartan/lib/List.thy    | 10 +++++-----
 spartan/lib/Maybe.thy   |  2 +-
 spartan/lib/Prelude.thy |  8 ++++----
 3 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'spartan/lib')

diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 34873e4..dd51582 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -45,7 +45,7 @@ where
 
 lemmas
   [form] = ListF and
-  [intro, intros] = List_nil List_cons and
+  [intr, intro] = List_nil List_cons and
   [elim "?xs"] = ListE and
   [comp] = List_comp_nil List_comp_cons
 
@@ -106,7 +106,7 @@ translations
   "head" \<leftharpoondown> "CONST List.head A"
   "tail" \<leftharpoondown> "CONST List.tail A"
 
-Lemma head_type [typechk]:
+Lemma head_type [type]:
   assumes "A: U i" "xs: List A"
   shows "head xs: Maybe A"
   unfolding head_def by typechk
@@ -116,7 +116,7 @@ Lemma head_of_cons [comp]:
   shows "head (x # xs) \<equiv> some x"
   unfolding head_def by reduce
 
-Lemma tail_type [typechk]:
+Lemma tail_type [type]:
   assumes "A: U i" "xs: List A"
   shows "tail xs: List A"
   unfolding tail_def by typechk
@@ -157,7 +157,7 @@ definition map_i ("map") where [implicit]: "map \<equiv> List.map ? ?"
 
 translations "map" \<leftharpoondown> "CONST List.map A B"
 
-Lemma map_type [typechk]:
+Lemma map_type [type]:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
   shows "map f xs: List B"
   unfolding map_def by typechk
@@ -177,7 +177,7 @@ definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
 
 translations "rev" \<leftharpoondown> "CONST List.rev A"
 
-Lemma rev_type [typechk]:
+Lemma rev_type [type]:
   assumes "A: U i" "xs: List A"
   shows "rev xs: List A"
   unfolding rev_def by typechk
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index a2e1638..0a7ec21 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -56,7 +56,7 @@ Lemma Maybe_comp_some:
 
 lemmas
   [form] = MaybeF and
-  [intro, intros] = Maybe_none Maybe_some and
+  [intr, intro] = Maybe_none Maybe_some and
   [comp] = Maybe_comp_none Maybe_comp_some and
   MaybeE [elim "?m"] = MaybeInd[rotated 4]
 lemmas
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
index 36f12d2..6adbce8 100644
--- a/spartan/lib/Prelude.thy
+++ b/spartan/lib/Prelude.thy
@@ -43,8 +43,8 @@ axiomatization where
 
 lemmas
   [form] = SumF and
-  [intro] = Sum_inl Sum_inr and
-  [intros] = Sum_inl[rotated] Sum_inr[rotated] and
+  [intr] = Sum_inl Sum_inr and
+  [intro] = Sum_inl[rotated] Sum_inr[rotated] and
   [elim ?s] = SumE and
   [comp] = Sum_comp_inl Sum_comp_inr
 
@@ -79,7 +79,7 @@ and
 
 lemmas
   [form] = TopF BotF and
-  [intro, intros] = TopI and
+  [intr, intro] = TopI and
   [elim ?a] = TopE and
   [elim ?x] = BotE and
   [comp] = Top_comp
@@ -129,7 +129,7 @@ Lemma if_false:
 
 lemmas
   [form] = BoolF and
-  [intro, intros] = Bool_true Bool_false and
+  [intr, intro] = Bool_true Bool_false and
   [comp] = if_true if_false and
   [elim ?x] = ifelse
 lemmas
-- 
cgit v1.2.3