# HG changeset patch
# User wenzelm
# Date 1452717866 -3600
# Node ID a817e4335a31f62b7cd872079f419b389730754b
# Parent  7eaeae127955d9e584f7c14a17b61cd7d111cc09
clarified example;

diff -r 7eaeae127955 -r a817e4335a31 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Jan 13 21:15:23 2016 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Jan 13 21:44:26 2016 +0100
@@ -1001,21 +1001,26 @@
 
 subsubsection \<open>Example\<close>
 
-consts null :: 'a
+consts Length :: "'a \<Rightarrow> nat"
 
 overloading
-  null_nat \<equiv> "null :: nat"
-  null_pair \<equiv> "null :: 'a \<times> 'b"
+  Length\<^sub>0 \<equiv> "Length :: unit \<Rightarrow> nat"
+  Length\<^sub>1 \<equiv> "Length :: 'a \<times> unit \<Rightarrow> nat"
+  Length\<^sub>2 \<equiv> "Length :: 'a \<times> 'b \<times> unit \<Rightarrow> nat"
+  Length\<^sub>3 \<equiv> "Length :: 'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat"
 begin
 
-definition null_nat :: nat
-  where "null_nat = 0"
-
-definition null_pair :: "'a \<times> 'b"
-  where "null_pair = (null :: 'a, null :: 'b)"
+fun Length\<^sub>0 :: "unit \<Rightarrow> nat" where "Length\<^sub>0 () = 0"
+fun Length\<^sub>1 :: "'a \<times> unit \<Rightarrow> nat" where "Length\<^sub>1 (a, ()) = 1"
+fun Length\<^sub>2 :: "'a \<times> 'b \<times> unit \<Rightarrow> nat" where "Length\<^sub>2 (a, b, ()) = 2"
+fun Length\<^sub>3 :: "'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat" where "Length\<^sub>3 (a, b, c, ()) = 3"
 
 end
 
+lemma "Length (a, b, c, ()) = 3" by simp
+lemma "Length ((a, b), (c, d), ()) = 2" by simp
+lemma "Length ((a, b, c, d, e), ()) = 1" by simp
+
 
 section \<open>Incorporating ML code \label{sec:ML}\<close>