src/HOL/Inductive.thy
changeset 23526 936dc616a7fb
parent 23389 aaca6a8e5414
child 23529 958f9d9cfb63
     1.1 --- a/src/HOL/Inductive.thy	Mon Jul 02 16:42:37 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Mon Jul 02 23:14:06 2007 +0200
     1.3 @@ -129,4 +129,27 @@
     1.4  
     1.5  use "Tools/primrec_package.ML"
     1.6  
     1.7 +text{* Lambda-abstractions with pattern matching: *}
     1.8 +
     1.9 +syntax
    1.10 +  "_fun_syntax":: "cases_syn => 'a => 'b"               ("(%_)" 10)
    1.11 +syntax (xsymbols)
    1.12 +  "_fun_syntax":: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
    1.13 +
    1.14 +ML{*
    1.15 +local
    1.16 +fun fun_tr ctxt [cs] =
    1.17 +  let val ft = DatatypeCase.case_tr DatatypePackage.datatype_of_constr ctxt
    1.18 +                 [Bound 0,cs]
    1.19 +  in Abs("", dummyT, ft) end;
    1.20 +in
    1.21 +val trfun_setup =
    1.22 +  Theory.add_advanced_trfuns ([],
    1.23 +    [("_fun_syntax", fun_tr)],
    1.24 +    [], []);
    1.25  end
    1.26 +*}
    1.27 +
    1.28 +setup trfun_setup
    1.29 +
    1.30 +end