--- a/src/HOL/Prod.ML Thu Oct 10 11:59:01 1996 +0200
+++ b/src/HOL/Prod.ML Thu Oct 10 12:00:23 1996 +0200
@@ -299,12 +299,6 @@
fst_imageE, snd_imageE, prod_fun_imageE,
Pair_inject];
-val prod_cs = set_cs addSIs [SigmaI, splitI, splitI2, mem_splitI, mem_splitI2]
- addIs [fst_imageI, snd_imageI, prod_fun_imageI]
- addSEs [SigmaE2, SigmaE, splitE, mem_splitE,
- fst_imageE, snd_imageE, prod_fun_imageE,
- Pair_inject];
-
structure Prod_Syntax =
struct
--- 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";