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