--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Tutorial/Datatype/Term.thy Thu Nov 12 16:45:40 1998 +0100
@@ -0,0 +1,16 @@
+Term = Main +
+datatype 'a t = A | B "'a * ('a t list)"
+datatype expr = Var string | Lam string expr | App expr expr
+ | Data data
+and data = Bool bool | Num nat
+ | Closure string expr "(string * data)list"
+datatype ('a,'b)term = Var 'a | App 'b ((('a,'b)term)list)
+consts
+ subst :: ('a => ('a,'b)term) => ('a,'b)term => ('a,'b)term
+ substs :: ('a => ('a,'b)term) => ('a,'b)term list => ('a,'b)term list
+primrec
+ "subst s (Var x) = s x"
+ "subst s (App f ts) = App f (substs s ts)"
+ "substs s [] = []"
+ "substs s (t # ts) = subst s t # substs s ts"
+end