src/HOL/Data_Structures/Queue_Spec.thy

--- a/src/HOL/Data_Structures/Queue_Spec.thy	Fri Oct 16 11:38:55 2020 +0200
+++ b/src/HOL/Data_Structures/Queue_Spec.thy	Fri Oct 16 15:09:41 2020 +0200
@@ -11,7 +11,7 @@
 locale Queue =
 fixes empty :: "'q"
 fixes enq :: "'a \<Rightarrow> 'q \<Rightarrow> 'q"
-fixes front :: "'q \<Rightarrow> 'a"
+fixes first :: "'q \<Rightarrow> 'a"
 fixes deq :: "'q \<Rightarrow> 'q"
 fixes is_empty :: "'q \<Rightarrow> bool"
 fixes list :: "'q \<Rightarrow> 'a list"
@@ -19,7 +19,7 @@
 assumes list_empty:    "list empty = []"
 assumes list_enq:      "invar q \<Longrightarrow> list(enq x q) = list q @ [x]"
 assumes list_deq:      "invar q \<Longrightarrow> list(deq q) = tl(list q)"
-assumes list_front:    "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> front q = hd(list q)"
+assumes list_first:    "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> first q = hd(list q)"
 assumes list_is_empty: "invar q \<Longrightarrow> is_empty q = (list q = [])"
 assumes invar_empty:   "invar empty"
 assumes invar_enq:     "invar q \<Longrightarrow> invar(enq x q)"