diff -r 0b2ff9541727 -r 1c519a3cca59 src/FOL/ex/List.thy
--- a/src/FOL/ex/List.thy	Sat Sep 03 16:50:22 2005 +0200
+++ b/src/FOL/ex/List.thy	Sat Sep 03 17:15:51 2005 +0200
@@ -2,48 +2,52 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
-
-Examples of simplification and induction on lists
 *)
 
-List = Nat2 +
+header {* Examples of simplification and induction on lists *}
 
-types 'a list
-arities list :: (term)term
+theory List
+imports Nat2
+begin
+
+typedecl 'a list
+arities list :: ("term") "term"
 
 consts
-   hd           :: 'a list => 'a  
-   tl           :: 'a list => 'a list
-   forall       :: ['a list, 'a => o] => o  
-   len          :: 'a list => nat  
-   at           :: ['a list, nat] => 'a  
-   Nil          :: ('a list)                         ("[]")
-   Cons         :: ['a, 'a list] => 'a list          (infixr "." 80)
-   "++"         :: ['a list, 'a list] => 'a list     (infixr 70)
+   hd           :: "'a list => 'a"
+   tl           :: "'a list => 'a list"
+   forall       :: "['a list, 'a => o] => o"
+   len          :: "'a list => nat"
+   at           :: "['a list, nat] => 'a"
+   Nil          :: "'a list"                          ("[]")
+   Cons         :: "['a, 'a list] => 'a list"         (infixr "." 80)
+   app          :: "['a list, 'a list] => 'a list"    (infixr "++" 70)
 
-rules
- list_ind "[| P([]);  ALL x l. P(l)-->P(x . l) |] ==> All(P)"
+axioms
+ list_ind: "[| P([]);  ALL x l. P(l)-->P(x . l) |] ==> All(P)"
 
- forall_cong 
+ forall_cong:
   "[| l = l';  !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"
 
- list_distinct1 "~[] = x . l"
- list_distinct2 "~x . l = []"
+ list_distinct1: "~[] = x . l"
+ list_distinct2: "~x . l = []"
+
+ list_free:      "x . l = x' . l' <-> x=x' & l=l'"
 
- list_free      "x . l = x' . l' <-> x=x' & l=l'"
+ app_nil:        "[]++l = l"
+ app_cons:       "(x . l)++l' = x .(l++l')"
+ tl_eq:  "tl(m . q) = q"
+ hd_eq:  "hd(m . q) = m"
 
- app_nil        "[]++l = l"
- app_cons       "(x . l)++l' = x .(l++l')"
- tl_eq  "tl(m . q) = q"
- hd_eq  "hd(m . q) = m"
+ forall_nil: "forall([],P)"
+ forall_cons: "forall(x . l,P) <-> P(x) & forall(l,P)"
 
- forall_nil "forall([],P)"
- forall_cons "forall(x . l,P) <-> P(x) & forall(l,P)"
+ len_nil: "len([]) = 0"
+ len_cons: "len(m . q) = succ(len(q))"
 
- len_nil "len([]) = 0"
- len_cons "len(m . q) = succ(len(q))"
+ at_0: "at(m . q,0) = m"
+ at_succ: "at(m . q,succ(n)) = at(q,n)"
 
- at_0 "at(m . q,0) = m"
- at_succ "at(m . q,succ(n)) = at(q,n)"
+ML {* use_legacy_bindings (the_context ()) *}
 
 end