diff -r f04b33ce250f -r a4dc62a46ee4 ex/Term.thy
--- a/ex/Term.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(*  Title: 	HOL/ex/Term
-    ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Terms over a given alphabet -- function applications; illustrates list functor
-  (essentially the same type as in Trees & Forests)
-
-There is no constructor APP because it is simply cons ($) 
-*)
-
-Term = SList +
-
-types   'a term
-
-arities term :: (term)term
-
-consts
-  term		:: "'a item set => 'a item set"
-  Rep_term	:: "'a term => 'a item"
-  Abs_term	:: "'a item => 'a term"
-  Rep_Tlist	:: "'a term list => 'a item"
-  Abs_Tlist	:: "'a item => 'a term list"
-  App		:: "['a, ('a term)list] => 'a term"
-  Term_rec	:: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b"
-  term_rec	:: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
-
-inductive "term(A)"
-  intrs
-    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
-  monos   "[list_mono]"
-
-defs
-  (*defining abstraction/representation functions for term list...*)
-  Rep_Tlist_def	"Rep_Tlist == Rep_map(Rep_term)"
-  Abs_Tlist_def	"Abs_Tlist == Abs_map(Abs_term)"
-
-  (*defining the abstract constants*)
-  App_def 	"App(a,ts) == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
-
-  (*list recursion*)
-  Term_rec_def	
-   "Term_rec(M,d) == wfrec(trancl(pred_sexp),  M, 
-            Split(%x y g. d(x,y, Abs_map(g,y))))"
-
-  term_rec_def
-   "term_rec(t,d) == 
-   Term_rec(Rep_term(t), %x y r. d(Inv(Leaf,x), Abs_Tlist(y), r))"
-
-rules
-    (*faking a type definition for term...*)
-  Rep_term 		"Rep_term(n): term(range(Leaf))"
-  Rep_term_inverse 	"Abs_term(Rep_term(t)) = t"
-  Abs_term_inverse 	"M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
-end