# HG changeset patch
# User wenzelm
# Date 910622528 -3600
# Node ID e2d2b896c717ccc6ac9a1a149985299bef1958ef
# Parent  3ad1364bbb4b56e33efa53c580db9c4eb174b69f
Object logic specific operations.

diff -r 3ad1364bbb4b -r e2d2b896c717 src/Pure/object_logic.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/object_logic.ML	Mon Nov 09 15:42:08 1998 +0100
@@ -0,0 +1,31 @@
+(*  Title:      Pure/object_logic.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Object logic specific operations.
+
+TODO:
+  - theory data instead of hardwired operations (!!);
+*)
+
+signature OBJECT_LOGIC =
+sig
+  val dest_statement: string * term -> (string * term) list
+  val setup: (theory -> theory) list
+end;
+
+structure ObjectLogic: OBJECT_LOGIC =
+struct
+
+
+fun dest_statement (name, prop) =
+  let val concl = Logic.strip_imp_concl prop in
+    [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
+      (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => [])
+  end;
+
+
+(* FIXME *)
+val setup = [];
+
+end;