# HG changeset patch
# User wenzelm
# Date 878555078 -3600
# Node ID 423d0d527cbc9cc33ca9f7e67a3f04e2258c9410
# Parent  f759352f669fce64f67840d186f9f9216f154be1
HOL theory data.

diff -r f759352f669f -r 423d0d527cbc src/HOL/thy_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/thy_data.ML	Mon Nov 03 12:04:38 1997 +0100
@@ -0,0 +1,47 @@
+(*  Title:      HOL/thy_data.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+HOL theory data.
+*)
+
+type datatype_info =
+ {case_const: term,
+  case_rewrites: thm list,
+  constructors: term list,
+  induct_tac: string -> int -> tactic,
+  nchotomy: thm,
+  exhaustion: thm,
+  exhaust_tac: string -> int -> tactic,
+  case_cong: thm};
+
+signature THY_DATA =
+sig
+  val datatypesK: string
+  val hol_data: (string * (exn * (exn -> exn) * (exn * exn -> exn) * (exn -> unit))) list
+end;
+
+structure ThyData: THY_DATA =
+struct
+
+
+(** datatypes **)	(* FIXME *)
+
+val datatypesK = "datatypes";
+exception DatatypeInfo of datatype_info Symtab.table;
+
+
+
+(** records **)		(* FIXME *)
+
+val recordsK = "records";
+
+
+
+(** hol_data **)
+
+val hol_data =
+ [Simplifier.simpset_thy_data, ClasetThyData.thy_data];
+
+
+end;