changeset 2089 | e2ec077ac90d |
parent 2031 | 03a843f0f447 |
child 2892 | 67fb21ddfe15 |
--- a/src/HOL/Sexp.ML Thu Oct 10 11:59:01 1996 +0200 +++ b/src/HOL/Sexp.ML Thu Oct 10 12:00:23 1996 +0200 @@ -38,8 +38,6 @@ by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1); qed "sexp_In1I"; -val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI]; - AddIs (sexp.intrs@[SigmaI, uprodI]); goal Sexp.thy "range(Leaf) <= sexp";