removed superfluous AddIs thms (were already in)
authoroheimb
Wed Sep 09 16:42:45 1998 +0200 (1998-09-09)
changeset 5440f099dffd0f18
parent 5439 2e0c18eedfd0
child 5441 45bd13b15d80
removed superfluous AddIs thms (were already in)
src/HOL/Sexp.ML
     1.1 --- a/src/HOL/Sexp.ML	Wed Sep 09 16:21:08 1998 +0200
     1.2 +++ b/src/HOL/Sexp.ML	Wed Sep 09 16:42:45 1998 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
     1.5  qed "sexp_In1I";
     1.6  
     1.7 -AddIs (sexp.intrs@[SigmaI, uprodI]);
     1.8 +AddIs sexp.intrs;
     1.9  
    1.10  Goal "range(Leaf) <= sexp";
    1.11  by (Blast_tac 1);