equal
deleted
inserted
replaced
88 seqcont_tr' (Const("SeqO'",_) $ f $ s) = |
88 seqcont_tr' (Const("SeqO'",_) $ f $ s) = |
89 Const("SeqContApp",dummyT) $ |
89 Const("SeqContApp",dummyT) $ |
90 (Const("SeqO",dummyT) $ f) $ |
90 (Const("SeqO",dummyT) $ f) $ |
91 (seqcont_tr' s) | |
91 (seqcont_tr' s) | |
92 (* seqcont_tr' ((a as Abs(_,_,_)) $ s)= |
92 (* seqcont_tr' ((a as Abs(_,_,_)) $ s)= |
93 seqcont_tr'(betapply(a,s)) | *) |
93 seqcont_tr'(Term.betapply(a,s)) | *) |
94 seqcont_tr' (i $ s) = |
94 seqcont_tr' (i $ s) = |
95 Const("SeqContApp",dummyT) $ |
95 Const("SeqContApp",dummyT) $ |
96 (Const("SeqId",dummyT) $ i) $ |
96 (Const("SeqId",dummyT) $ i) $ |
97 (seqcont_tr' s); |
97 (seqcont_tr' s); |
98 |
98 |
101 Const("SeqEmp",dummyT) | |
101 Const("SeqEmp",dummyT) | |
102 seq_itr' (Const("SeqO'",_) $ f $ s) = |
102 seq_itr' (Const("SeqO'",_) $ f $ s) = |
103 Const("SeqApp",dummyT) $ |
103 Const("SeqApp",dummyT) $ |
104 (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) | |
104 (Const("SeqO",dummyT) $ f) $ (seqcont_tr' s) | |
105 (* seq_itr' ((a as Abs(_,_,_)) $ s) = |
105 (* seq_itr' ((a as Abs(_,_,_)) $ s) = |
106 seq_itr'(betapply(a,s)) | *) |
106 seq_itr'(Term.betapply(a,s)) | *) |
107 seq_itr' (i $ s) = |
107 seq_itr' (i $ s) = |
108 Const("SeqApp",dummyT) $ |
108 Const("SeqApp",dummyT) $ |
109 (Const("SeqId",dummyT) $ i) $ |
109 (Const("SeqId",dummyT) $ i) $ |
110 (seqcont_tr' s) |
110 (seqcont_tr' s) |
111 in case s of |
111 in case s of |