diff -r 000000000000 -r a5a9c433f639 src/Cube/Cube.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/Cube.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,60 @@
+(*  Title:      Cube/cube.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1993  University of Cambridge
+
+Barendregt's Lambda-Cube
+*)
+
+Cube = Pure +
+
+types
+  term, context, typing 0
+
+arities
+  term :: logic
+
+consts
+  Abs, Prod     :: "[term, term => term] => term"
+  Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
+  Trueprop1     :: "typing => prop"                     ("(_)")
+  MT_context    :: "context"                            ("")
+  ""            :: "id => context"                      ("_ ")
+  ""            :: "var => context"                     ("_ ")
+  Context       :: "[typing, context] => context"       ("_ _")
+  star          :: "term"                               ("*")
+  box           :: "term"                               ("[]")
+  "^"           :: "[term, term] => term"               (infixl 20)
+  Lam           :: "[id, term, term] => term"           ("(3Lam _:_./ _)" [0, 0, 0] 10)
+  Pi            :: "[id, term, term] => term"           ("(3Pi _:_./ _)" [0, 0] 10)
+  "->"          :: "[term, term] => term"               (infixr 10)
+  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
+
+translations
+  (prop) "x:X"  == (prop) "|- x:X"
+  "Lam x:A. B"  == "Abs(A, %x. B)"
+  "Pi x:A. B"   => "Prod(A, %x. B)"
+
+rules
+  s_b           "*: []"
+
+  strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
+  strip_b       "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
+
+  app           "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
+
+  pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
+
+  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
+\                   ==> Abs(A, f) : Prod(A, B)"
+
+  beta          "Abs(A, f)^a == f(a)"
+
+end
+
+
+ML
+
+val parse_translation = [("op ->", ndependent_tr "Prod")];
+val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
+