--- a/src/Doc/Datatypes/Datatypes.thy Sun Apr 07 12:44:37 2019 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Sun Apr 07 08:26:57 2019 +0200
@@ -13,12 +13,16 @@
imports
Setup
"HOL-Library.BNF_Axiomatization"
- "HOL-Library.Cardinal_Notations"
"HOL-Library.Countable"
"HOL-Library.FSet"
"HOL-Library.Simps_Case_Conv"
begin
+
+(*<*)
+unbundle cardinal_syntax
+(*>*)
+
section \<open>Introduction
\label{sec:introduction}\<close>
@@ -2761,8 +2765,8 @@
text \<open>
The example below shows how to register a type as a BNF using the @{command bnf}
-command. Some of the proof obligations are best viewed with the theory
-\<^file>\<open>~~/src/HOL/Library/Cardinal_Notations.thy\<close> imported.
+command. Some of the proof obligations are best viewed with the bundle
+"cardinal_syntax" included.
The type is simply a copy of the function space \<^typ>\<open>'d \<Rightarrow> 'a\<close>, where \<^typ>\<open>'a\<close>
is live and \<^typ>\<open>'d\<close> is dead. We introduce it together with its map function,