--- a/src/HOL/String.thy Tue Aug 18 21:45:24 2020 +0100
+++ b/src/HOL/String.thy Wed Aug 19 12:58:28 2020 +0100
@@ -158,7 +158,7 @@
proof -
have "range (of_char :: char \<Rightarrow> nat) = of_char ` char_of ` {0::nat..<256}"
by (auto simp add: range_nat_of_char intro!: image_eqI)
- with inj_of_char [where ?'a = nat] show ?thesis
+ with inj_of_char [where ?'a = nat] show ?thesis
by (simp add: inj_image_eq_iff)
qed
@@ -523,16 +523,16 @@
begin
qualified lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
- is "order.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
+ is "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
.
qualified lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
- is "order.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
+ is "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
.
instance proof -
- from linorder_char interpret linorder "order.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
- "order.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
+ from linorder_char interpret linorder "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
+ "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
by (rule linorder.lexordp_linorder)
show "PROP ?thesis"
by (standard; transfer) (simp_all add: less_le_not_le linear)
@@ -602,7 +602,7 @@
fix cs
assume "\<forall>c\<in>set cs. \<not> digit7 c"
then show "map (String.ascii_of \<circ> char_of) (map of_char cs) = cs"
- by (induction cs) (simp_all add: String.ascii_of_idem)
+ by (induction cs) (simp_all add: String.ascii_of_idem)
qed
qualified lemma explode_code [code]:
@@ -628,7 +628,7 @@
text \<open>Alternative constructor for generated computations\<close>
context
-begin
+begin
qualified definition Literal' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
where [simp]: "Literal' = String.Literal"