--- a/src/HOL/Datatype.ML Fri Oct 26 23:59:13 2001 +0200
+++ b/src/HOL/Datatype.ML Sat Oct 27 00:00:05 2001 +0200
@@ -1,9 +1,68 @@
(* Title: HOL/Datatype.ML
ID: $Id$
- Author: Stefan Berghofer
- Copyright 1999 TU Muenchen
+ Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
+(** legacy ML bindings **)
+
+structure bool =
+struct
+ val distinct = thms "bool.distinct";
+ val inject = thms "bool.inject";
+ val exhaust = thm "bool.exhaust";
+ val cases = thms "bool.cases";
+ val split = thm "bool.split";
+ val split_asm = thm "bool.split_asm";
+ val induct = thm "bool.induct";
+ val recs = thms "bool.recs";
+ val simps = thms "bool.simps";
+ val size = thms "bool.size";
+end;
+
+structure sum =
+struct
+ val distinct = thms "sum.distinct";
+ val inject = thms "sum.inject";
+ val exhaust = thm "sum.exhaust";
+ val cases = thms "sum.cases";
+ val split = thm "sum.split";
+ val split_asm = thm "sum.split_asm";
+ val induct = thm "sum.induct";
+ val recs = thms "sum.recs";
+ val simps = thms "sum.simps";
+ val size = thms "sum.size";
+end;
+
+structure unit =
+struct
+ val distinct = thms "unit.distinct";
+ val inject = thms "unit.inject";
+ val exhaust = thm "unit.exhaust";
+ val cases = thms "unit.cases";
+ val split = thm "unit.split";
+ val split_asm = thm "unit.split_asm";
+ val induct = thm "unit.induct";
+ val recs = thms "unit.recs";
+ val simps = thms "unit.simps";
+ val size = thms "unit.size";
+end;
+
+structure prod =
+struct
+ val distinct = thms "prod.distinct";
+ val inject = thms "prod.inject";
+ val exhaust = thm "prod.exhaust";
+ val cases = thms "prod.cases";
+ val split = thm "prod.split";
+ val split_asm = thm "prod.split_asm";
+ val induct = thm "prod.induct";
+ val recs = thms "prod.recs";
+ val simps = thms "prod.simps";
+ val size = thms "prod.size";
+end;
+
+
(** sum_case -- the selection operator for sums **)
(*compatibility*)
@@ -12,7 +71,7 @@
bind_thm ("sum_case_Inr", sum_case_Inr);
Goal "sum_case (%x::'a. f(Inl x)) (%y::'b. f(Inr y)) s = f(s)";
-by (EVERY1 [res_inst_tac [("s","s")] sumE,
+by (EVERY1 [res_inst_tac [("s","s")] sumE,
etac ssubst, rtac sum_case_Inl,
etac ssubst, rtac sum_case_Inr]);
qed "surjective_sum";