--- a/src/FOL/ex/List.thy Fri Feb 02 12:05:24 1996 +0100
+++ b/src/FOL/ex/List.thy Mon Feb 05 13:44:28 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/list
+(* Title: FOL/ex/list
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1991 University of Cambridge
Examples of simplification and induction on lists
@@ -12,14 +12,14 @@
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
- "[]" :: ('a list) ("[]")
- "." :: ['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
+ "[]" :: ('a list) ("[]")
+ "." :: ['a, 'a list] => 'a list (infixr 80)
+ "++" :: ['a list, 'a list] => 'a list (infixr 70)
rules
list_ind "[| P([]); ALL x l. P(l)-->P(x.l) |] ==> All(P)"
@@ -30,12 +30,12 @@
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)"