From aff3d43d9865e7b8d082f0c239d2c73eee1fb291 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 21 Jan 2021 00:52:13 +0000
Subject: renamings

---
 spartan/lib/List.thy | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'spartan/lib/List.thy')

diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 1501221..4beb9b6 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -114,7 +114,7 @@ Lemma head_type [type]:
 Lemma head_of_cons [comp]:
   assumes "A: U i" "x: A" "xs: List A"
   shows "head (x # xs) \<equiv> some x"
-  unfolding head_def by reduce
+  unfolding head_def by compute
 
 Lemma tail_type [type]:
   assumes "A: U i" "xs: List A"
@@ -124,7 +124,7 @@ Lemma tail_type [type]:
 Lemma tail_of_cons [comp]:
   assumes "A: U i" "x: A" "xs: List A"
   shows "tail (x # xs) \<equiv> xs"
-  unfolding tail_def by reduce
+  unfolding tail_def by compute
 
 subsection \<open>Append\<close>
 
@@ -185,7 +185,7 @@ Lemma rev_type [type]:
 Lemma rev_nil [comp]:
   assumes "A: U i"
   shows "rev (nil A) \<equiv> nil A"
-  unfolding rev_def by reduce
+  unfolding rev_def by compute
 
 
 end
-- 
cgit v1.2.3

