src/Doc/Datatypes/Datatypes.thy

--- a/src/Doc/Datatypes/Datatypes.thy	Mon May 12 17:17:32 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue May 13 09:21:22 2014 +0200
@@ -10,7 +10,7 @@
 theory Datatypes
 imports
   Setup
-  "~~/src/HOL/Library/BNF_Decl"
+  "~~/src/HOL/Library/BNF_Axiomatization"
   "~~/src/HOL/Library/Cardinal_Notations"
   "~~/src/HOL/Library/FSet"
   "~~/src/HOL/Library/Simps_Case_Conv"
@@ -80,7 +80,7 @@
 infinite branching.
 
 The package is part of @{theory Main}. Additional functionality is provided by
-the theory @{theory BNF_Decl}, located in the directory
+the theory @{theory BNF_Axiomatization}, located in the directory
 \verb|~~/src/HOL/Library|.
 
 The package, like its predecessor, fully adheres to the LCF philosophy
@@ -2477,7 +2477,7 @@
 for further examples of BNF registration, some of which feature custom
 witnesses.
 
-The next example declares a BNF axiomatically. The @{command bnf_decl} command
+The next example declares a BNF axiomatically. The @{command bnf_axiomatization} command
 introduces a type @{text "('a, 'b, 'c) F"}, three set constants, a map
 function, a relator, and a nonemptiness witness that depends only on
 @{typ 'a}. (The type @{text "'a \<Rightarrow> ('a, 'b, 'c) F"} of
@@ -2486,7 +2486,7 @@
 properties are postulated as axioms.
 *}
 
-    bnf_decl (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
+    bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
 
 text {* \blankline *}
 
@@ -2533,11 +2533,11 @@
 
 text {*
 \begin{matharray}{rcl}
-  @{command_def "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
+  @{command_def "bnf_axiomatization"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}
 
 @{rail \<open>
-  @@{command bnf_decl} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
+  @@{command bnf_axiomatization} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
     @{syntax wit_types}? mixfix?
   ;
   @{syntax_def wit_types}: '[' 'wits' ':' types ']'
@@ -2546,7 +2546,7 @@
 \medskip
 
 \noindent
-The @{command bnf_decl} command declares a new type and associated constants
+The @{command bnf_axiomatization} command declares a new type and associated constants
 (map, set, relator, and cardinal bound) and asserts the BNF properties for
 these constants as axioms.
 
@@ -2558,12 +2558,12 @@
 Type arguments are live by default; they can be marked as dead by entering
 ``-'' (hyphen) instead of an identifier for the corresponding set function.
 Witnesses can be specified by their types. Otherwise, the syntax of
-@{command bnf_decl} is identical to the left-hand side of a
+@{command bnf_axiomatization} is identical to the left-hand side of a
 @{command datatype_new} or @{command codatatype} definition.
 
 The command is useful to reason abstractly about BNFs. The axioms are safe
 because there exists BNFs of arbitrary large arities. Applications must import
-the theory @{theory BNF_Decl}, located in the directory
+the theory @{theory BNF_Axiomatization}, located in the directory
 \verb|~~/src/HOL/Library|, to use this functionality.
 *}