| changeset 2950 | 0911cb7bf696 |
| parent 2943 | 09834ba7ce59 |
| child 3235 | 5ebd327ffb96 |
| 2949:adf22ee09738 | 2950:0911cb7bf696 |
|---|---|
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype trm = |
7 nominal_datatype trm = |
8 Var "name" |
8 Var "name" |
9 | App "trm" "trm" |
9 | App "trm" "trm" |
10 | Let x::"name" "trm" t::"trm" bind x in t |
10 | Let x::"name" "trm" t::"trm" binds x in t |
11 |
11 |
12 print_theorems |
12 print_theorems |
13 |
13 |
14 thm trm.fv_defs |
14 thm trm.fv_defs |
15 thm trm.eq_iff |
15 thm trm.eq_iff |