| changeset 66453 | cc19f7ca2ed6 |
| parent 63167 | 0909deb8059b |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
6 (* *) |
6 (* *) |
7 (* Polishing Up the Tait-Martin Löf Proof of the *) |
7 (* Polishing Up the Tait-Martin Löf Proof of the *) |
8 (* Church-Rosser Theorem (1995). *) |
8 (* Church-Rosser Theorem (1995). *) |
9 |
9 |
10 theory CR_Takahashi |
10 theory CR_Takahashi |
11 imports "../Nominal" |
11 imports "HOL-Nominal.Nominal" |
12 begin |
12 begin |
13 |
13 |
14 atom_decl name |
14 atom_decl name |
15 |
15 |
16 nominal_datatype lam = |
16 nominal_datatype lam = |