Nominal/Ex/Multi_Recs2.thy
changeset 2950 0911cb7bf696
parent 2787 1a6593bc494d
child 3071 11f6a561eb4b
child 3231 188826f1ccdb
equal deleted inserted replaced
2949:adf22ee09738 2950:0911cb7bf696
    15 
    15 
    16 nominal_datatype fun_recs: exp =
    16 nominal_datatype fun_recs: exp =
    17   Var name
    17   Var name
    18 | Unit 
    18 | Unit 
    19 | Pair exp exp
    19 | Pair exp exp
    20 | LetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
    20 | LetRec l::lrbs e::exp binds (set) "b_lrbs l" in l e
    21 and fnclause =
    21 and fnclause =
    22   K x::name p::pat f::exp bind (set) "b_pat p" in f
    22   K x::name p::pat f::exp binds (set) "b_pat p" in f
    23 and fnclauses =
    23 and fnclauses =
    24   S fnclause
    24   S fnclause
    25 | ORs fnclause fnclauses
    25 | ORs fnclause fnclauses
    26 and lrb =
    26 and lrb =
    27   Clause fnclauses
    27   Clause fnclauses