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) \ 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) \ xs" - unfolding tail_def by reduce + unfolding tail_def by compute subsection \Append\ @@ -185,7 +185,7 @@ Lemma rev_type [type]: Lemma rev_nil [comp]: assumes "A: U i" shows "rev (nil A) \ nil A" - unfolding rev_def by reduce + unfolding rev_def by compute end -- cgit v1.2.3