# HG changeset patch
# User nipkow
# Date 1183410846 -7200
# Node ID 936dc616a7fba1c7b07b785392ee1b7237988106
# Parent  c7ded89c2de0de0ec58cff88ea01bd9162125653
Added pattern maatching for lambda abstraction

diff -r c7ded89c2de0 -r 936dc616a7fb src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Jul 02 16:42:37 2007 +0200
+++ b/src/HOL/Inductive.thy	Mon Jul 02 23:14:06 2007 +0200
@@ -129,4 +129,27 @@
 
 use "Tools/primrec_package.ML"
 
+text{* Lambda-abstractions with pattern matching: *}
+
+syntax
+  "_fun_syntax":: "cases_syn => 'a => 'b"               ("(%_)" 10)
+syntax (xsymbols)
+  "_fun_syntax":: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
+
+ML{*
+local
+fun fun_tr ctxt [cs] =
+  let val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt
+                 [Bound 0,cs]
+  in Abs("", dummyT, ft) end;
+in
+val trfun_setup =
+  Theory.add_advanced_trfuns ([],
+    [("_fun_syntax", fun_tr)],
+    [], []);
 end
+*}
+
+setup trfun_setup
+
+end