diff options
Diffstat (limited to 'spartan/lib/List.thy')
| -rw-r--r-- | spartan/lib/List.thy | 6 |
1 files changed, 3 insertions, 3 deletions
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 |