changeset 2950 | 0911cb7bf696 |
parent 2787 | 1a6593bc494d |
child 3071 | 11f6a561eb4b |
child 3231 | 188826f1ccdb |
--- a/Nominal/Ex/Multi_Recs2.thy Tue Jul 05 18:01:54 2011 +0200 +++ b/Nominal/Ex/Multi_Recs2.thy Tue Jul 05 18:42:34 2011 +0200 @@ -17,9 +17,9 @@ Var name | Unit | Pair exp exp -| LetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e +| LetRec l::lrbs e::exp binds (set) "b_lrbs l" in l e and fnclause = - K x::name p::pat f::exp bind (set) "b_pat p" in f + K x::name p::pat f::exp binds (set) "b_pat p" in f and fnclauses = S fnclause | ORs fnclause fnclauses