tuned document;

--- a/src/HOL/ex/Abstract_NAT.thy	Tue Aug 30 17:50:41 2011 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy	Tue Aug 30 17:51:30 2011 +0200
@@ -1,4 +1,4 @@
-(*
+(*  Title:      HOL/ex/Abstract_NAT.thy
     Author:     Makarius
 *)
 
@@ -25,8 +25,7 @@
 
 text {* \medskip Primitive recursion as a (functional) relation -- polymorphic! *}
 
-inductive
-  Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
+inductive Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
   for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
 where
     Rec_zero: "Rec e r zero e"
@@ -64,9 +63,8 @@
 
 text {* \medskip The recursion operator -- polymorphic! *}
 
-definition
-  rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a" where
-  "rec e r x = (THE y. Rec e r x y)"
+definition rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
+  where "rec e r x = (THE y. Rec e r x y)"
 
 lemma rec_eval:
   assumes Rec: "Rec e r x y"
@@ -90,9 +88,8 @@
 
 text {* \medskip Example: addition (monomorphic) *}
 
-definition
-  add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n" where
-  "add m n = rec n (\<lambda>_ k. succ k) m"
+definition add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
+  where "add m n = rec n (\<lambda>_ k. succ k) m"
 
 lemma add_zero [simp]: "add zero n = n"
   and add_succ [simp]: "add (succ m) n = succ (add m n)"
@@ -114,9 +111,8 @@
 
 text {* \medskip Example: replication (polymorphic) *}
 
-definition
-  repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list" where
-  "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
+definition repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
+  where "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
 
 lemma repl_zero [simp]: "repl zero x = []"
   and repl_succ [simp]: "repl (succ n) x = x # repl n x"
@@ -140,9 +136,11 @@
     and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
   show "P n"
   proof (induct n)
-    case 0 show ?case by (rule zero)
+    case 0
+    show ?case by (rule zero)
   next
-    case Suc then show ?case by (rule succ)
+    case Suc
+    then show ?case by (rule succ)
   qed
 qed
 

--- a/src/HOL/ex/Antiquote.thy	Tue Aug 30 17:50:41 2011 +0200
+++ b/src/HOL/ex/Antiquote.thy	Tue Aug 30 17:51:30 2011 +0200
@@ -13,17 +13,15 @@
   syntax.
 *}
 
-syntax
-  "_Expr" :: "'a => 'a"    ("EXPR _" [1000] 999)
-
-definition
-  var :: "'a => ('a => nat) => nat"    ("VAR _" [1000] 999)
+definition var :: "'a => ('a => nat) => nat"  ("VAR _" [1000] 999)
   where "var x env = env x"
 
-definition
-  Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
+definition Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
   where "Expr exp env = exp env"
 
+syntax
+  "_Expr" :: "'a => 'a"  ("EXPR _" [1000] 999)
+
 parse_translation {*
   [Syntax_Trans.quote_antiquote_tr
     @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]