Deleted obsolete clasets
authorpaulson
Thu Oct 10 12:00:23 1996 +0200 (1996-10-10)
changeset 2089e2ec077ac90d
parent 2088 e814e03bbbb2
child 2090 307ebbbec862
Deleted obsolete clasets
src/HOL/Prod.ML
src/HOL/Sexp.ML
     1.1 --- a/src/HOL/Prod.ML	Thu Oct 10 11:59:01 1996 +0200
     1.2 +++ b/src/HOL/Prod.ML	Thu Oct 10 12:00:23 1996 +0200
     1.3 @@ -299,12 +299,6 @@
     1.4          fst_imageE, snd_imageE, prod_fun_imageE,
     1.5          Pair_inject];
     1.6  
     1.7 -val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2] 
     1.8 -                     addIs  [fst_imageI, snd_imageI, prod_fun_imageI]
     1.9 -                     addSEs [SigmaE2, SigmaE, splitE, mem_splitE, 
    1.10 -                             fst_imageE, snd_imageE, prod_fun_imageE,
    1.11 -                             Pair_inject];
    1.12 -
    1.13  structure Prod_Syntax =
    1.14  struct
    1.15  
     2.1 --- a/src/HOL/Sexp.ML	Thu Oct 10 11:59:01 1996 +0200
     2.2 +++ b/src/HOL/Sexp.ML	Thu Oct 10 12:00:23 1996 +0200
     2.3 @@ -38,8 +38,6 @@
     2.4  by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
     2.5  qed "sexp_In1I";
     2.6  
     2.7 -val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
     2.8 -
     2.9  AddIs (sexp.intrs@[SigmaI, uprodI]);
    2.10  
    2.11  goal Sexp.thy "range(Leaf) <= sexp";