--- a/src/HOL/MiniML/Instance.ML Fri Feb 14 15:32:00 1997 +0100
+++ b/src/HOL/MiniML/Instance.ML Fri Feb 14 16:01:43 1997 +0100
@@ -15,6 +15,7 @@
qed "bound_typ_inst_mk_scheme";
Addsimps [bound_typ_inst_mk_scheme];
+
goal thy "!!S. bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
by (type_scheme.induct_tac "sch" 1);
by (ALLGOALS Asm_full_simp_tac);
@@ -27,6 +28,7 @@
qed "bound_typ_inst_eq";
+
(* lemmatas for bound_scheme_inst *)
goal thy "!!t. bound_scheme_inst B (mk_scheme t) = mk_scheme t";