equal
deleted
inserted
replaced
5 |
5 |
6 Terms over a given alphabet -- function applications; illustrates list functor |
6 Terms over a given alphabet -- function applications; illustrates list functor |
7 (essentially the same type as in Trees & Forests) |
7 (essentially the same type as in Trees & Forests) |
8 *) |
8 *) |
9 |
9 |
10 open Term; |
10 (** Monotonicity and unfolding of the function **) |
11 |
|
12 (*** Monotonicity and unfolding of the function ***) |
|
13 |
11 |
14 Goal "term(A) = A <*> list(term(A))"; |
12 Goal "term(A) = A <*> list(term(A))"; |
15 by (fast_tac (claset() addSIs term.intrs |
13 by (fast_tac (claset() addSIs term.intrs |
16 addEs [term.elim]) 1); |
14 addEs [term.elim]) 1); |
17 qed "term_unfold"; |
15 qed "term_unfold"; |