# HG changeset patch
# User traytel
# Date 1362172531 -3600
# Node ID c1cb872ccb2bbe97f336282da2b116457a44f2d9
# Parent  4a92178011e7138d2c7b76a5d8c029e984eb4fc3
coercion-invariant arguments at work

diff -r 4a92178011e7 -r c1cb872ccb2b src/HOL/ex/Coercion_Examples.thy
--- a/src/HOL/ex/Coercion_Examples.thy	Fri Mar 01 22:15:31 2013 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy	Fri Mar 01 22:15:31 2013 +0100
@@ -178,4 +178,22 @@
 
 term "ys=[[[[[1::nat]]]]]"
 
+consts
+  case_nil :: "'a \<Rightarrow> 'b"
+  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
+  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
+
+declare [[coercion_args case_cons - -]]
+declare [[coercion_args case_abs -]]
+declare [[coercion_args case_elem - +]]
+
+term "case_cons (case_abs (\<lambda>n. case_abs (\<lambda>is. case_elem (((n::nat),(is::int list))) (n#is)))) case_nil"
+
+consts n :: nat m :: nat
+term "- (n + m)"
+declare [[coercion_args uminus -]]
+declare [[coercion_args plus + +]]
+term "- (n + m)"
+ 
 end