equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = recursive := true *} |
7 ML {* val _ = recursive := true *} |
|
8 ML {* val _ = alpha_type := AlphaGen *} |
8 nominal_datatype lam' = |
9 nominal_datatype lam' = |
9 VAR' "name" |
10 VAR' "name" |
10 | APP' "lam'" "lam'" |
11 | APP' "lam'" "lam'" |
11 | LAM' x::"name" t::"lam'" bind x in t |
12 | LAM' x::"name" t::"lam'" bind x in t |
12 | LET' bp::"bp'" t::"lam'" bind "bi' bp" in t |
13 | LET' bp::"bp'" t::"lam'" bind "bi' bp" in t |