# HG changeset patch
# User nipkow
# Date 1605777071 -3600
# Node ID a17c17ab931ca11fb976a38cc58abfa0d5cd902f
# Parent  c88e9369a7724d3a5ef40b6d67ef319aedc98474
tuned terminology

diff -r c88e9369a772 -r a17c17ab931c src/Doc/Prog_Prove/Bool_nat_list.thy
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Wed Nov 18 21:53:58 2020 +0100
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Nov 19 10:11:11 2020 +0100
@@ -438,7 +438,7 @@
 theory \<^theory>\<open>Complex_Main\<close> instead of \<^theory>\<open>Main\<close>.
 \end{warn}
 
-There are three conversion functions, meaning inclusions:
+There are three coercion functions that are inclusions and do not lose information:
 \begin{quote}
 \begin{tabular}{rcl}
 \<^const>\<open>int\<close> &\<open>::\<close>& \<^typ>\<open>nat \<Rightarrow> int\<close>\\
@@ -447,7 +447,7 @@
 \end{tabular}
 \end{quote}
 
-Isabelle inserts these conversion functions automatically once you import \<open>Complex_Main\<close>.
+Isabelle inserts these inclusions automatically once you import \<open>Complex_Main\<close>.
 If there are multiple type-correct completions, Isabelle chooses an arbitrary one.
 For example, the input \noquotes{@{term[source] "(i::int) + (n::nat)"}} has the unique
 type-correct completion \<^term>\<open>(i::int) + int(n::nat)\<close>. In contrast,