equal
deleted
inserted
replaced
9 |
9 |
10 declare [[STEPS = 9]] |
10 declare [[STEPS = 9]] |
11 |
11 |
12 nominal_datatype trm = |
12 nominal_datatype trm = |
13 Ax "name" "coname" |
13 Ax "name" "coname" |
14 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind_set n in t1, bind_set c in t2 |
14 | Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 |
15 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind_set c1 in t1, bind_set c2 in t2 |
15 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
16 | AndL1 n::"name" t::"trm" "name" bind_set n in t |
16 | AndL1 n::"name" t::"trm" "name" bind n in t |
17 | AndL2 n::"name" t::"trm" "name" bind_set n in t |
17 | AndL2 n::"name" t::"trm" "name" bind n in t |
18 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind_set c in t1, bind_set n in t2 |
18 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
19 | ImpR c::"coname" n::"name" t::"trm" "coname" bind_set n c in t |
19 | ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t |
20 |
20 |
21 thm alpha_trm_raw.intros[no_vars] |
21 thm alpha_trm_raw.intros[no_vars] |
22 |
22 |
23 (* |
23 (* |
24 thm trm.fv |
24 thm trm.fv |