Initial revision

[helm.git] / helm / interface / theory.ml

diff --git a/helm/interface/theory.ml b/helm/interface/theory.ml
new file mode 100644 (file)
index 0000000..be5b288
--- /dev/null
+++ b/helm/interface/theory.ml
@@ -0,0 +1,9 @@
+type theory_elem =
+   Theorem of string                    (* uri *)
+ | Definition of string                 (* uri *)
+ | Axiom of string                      (* uri *)
+ | Variable of string                   (* uri *)
+ | Section of string * theory_elem list (* uri, subtheory *)
+and theory =
+ string * theory_elem list              (* uri, subtheory *)
+;;