# HG changeset patch
# User wenzelm
# Date 918058984 -3600
# Node ID 328b4377755c06620c2b9a510d41e2fa17fde5a2
# Parent  7306d37f79298e9dcb402fe98be7ac4095674666
Theory presentation (fake implementation);

diff -r 7306d37f7929 -r 328b4377755c src/Pure/Thy/present.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/present.ML	Wed Feb 03 17:23:04 1999 +0100
@@ -0,0 +1,28 @@
+(*  Title:      Pure/Thy/present.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Theory presentation.            (* FIXME fake implementation *)
+*)
+
+signature BASIC_PRESENT =
+sig
+  val section: string -> unit
+end;
+
+signature PRESENT =
+sig
+  include BASIC_PRESENT
+  val thm: string -> thm -> unit
+end;
+
+structure Present: PRESENT =
+struct
+
+fun section _ = ();
+fun thm _ _ = ();
+
+end;
+
+structure BasicPresent: BASIC_PRESENT = Present;
+open BasicPresent;