# HG changeset patch
# User lcp
# Date 774087232 -7200
# Node ID 22325fd7234e81ccaf97a73237087cd1bc5fa0c9
# Parent  6cb6dd05d761ac2d4c415d7a11a680bcb340b0b3
indentation and renaming of rules

diff -r 6cb6dd05d761 -r 22325fd7234e doc-src/Logics/Old_HOL.tex
--- a/doc-src/Logics/Old_HOL.tex	Tue Jul 12 18:38:39 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Wed Jul 13 10:13:52 1994 +0200
@@ -648,10 +648,9 @@
 \tdx{subsetCE}        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P
 
 \tdx{subset_refl}     A <= A
-\tdx{subset_antisym}  [| A <= B;  B <= A |] ==> A = B
 \tdx{subset_trans}    [| A<=B;  B<=C |] ==> A<=C
 
-\tdx{set_ext}         [| !!x. (x:A) = (x:B) |] ==> A = B
+\tdx{equalityI}       [| A <= B;  B <= A |] ==> A = B
 \tdx{equalityD1}      A = B ==> A<=B
 \tdx{equalityD2}      A = B ==> B<=A
 \tdx{equalityE}       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
@@ -1156,35 +1155,35 @@
 
 \begin{figure}
 \begin{ttbox}\makeatother
-\tdx{list_rec_Nil}      list_rec([],c,h) = c  
-\tdx{list_rec_Cons}     list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h))
+\tdx{list_rec_Nil}    list_rec([],c,h) = c  
+\tdx{list_rec_Cons}   list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))
 
-\tdx{list_case_Nil}     list_case([],c,h) = c 
-\tdx{list_case_Cons}    list_case(x # xs, c, h) = h(x, xs)
+\tdx{list_case_Nil}   list_case([],c,h) = c 
+\tdx{list_case_Cons}  list_case(x#xs, c, h) = h(x, xs)
 
-\tdx{map_Nil}           map(f,[]) = []
-\tdx{map_Cons}          map(f, x \# xs) = f(x) \# map(f,xs)
+\tdx{map_Nil}         map(f,[]) = []
+\tdx{map_Cons}        map(f, x \# xs) = f(x) \# map(f,xs)
 
-\tdx{null_Nil}          null([]) = True
-\tdx{null_Cons}         null(x # xs) = False
+\tdx{null_Nil}        null([]) = True
+\tdx{null_Cons}       null(x#xs) = False
 
-\tdx{hd_Cons}           hd(x # xs) = x
-\tdx{tl_Cons}           tl(x # xs) = xs
+\tdx{hd_Cons}         hd(x#xs) = x
+\tdx{tl_Cons}         tl(x#xs) = xs
 
-\tdx{ttl_Nil}           ttl([]) = []
-\tdx{ttl_Cons}          ttl(x # xs) = xs
+\tdx{ttl_Nil}         ttl([]) = []
+\tdx{ttl_Cons}        ttl(x#xs) = xs
 
-\tdx{append_Nil}        [] @ ys = ys
-\tdx{append_Cons}       (x # xs) \at ys = x # xs \at ys
+\tdx{append_Nil}      [] @ ys = ys
+\tdx{append_Cons}     (x#xs) \at ys = x # xs \at ys
 
-\tdx{mem_Nil}           x mem [] = False
-\tdx{mem_Cons}          x mem y # ys = if(y = x, True, x mem ys)
+\tdx{mem_Nil}         x mem [] = False
+\tdx{mem_Cons}        x mem (y#ys) = if(y=x, True, x mem ys)
 
-\tdx{filter_Nil}        filter(P, []) = []
-\tdx{filter_Cons}       filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs))
+\tdx{filter_Nil}      filter(P, []) = []
+\tdx{filter_Cons}     filter(P,x#xs) = if(P(x), x#filter(P,xs), filter(P,xs))
 
-\tdx{list_all_Nil}      list_all(P,[]) = True
-\tdx{list_all_Cons}     list_all(P, x # xs) = (P(x) & list_all(P, xs))
+\tdx{list_all_Nil}    list_all(P,[]) = True
+\tdx{list_all_Cons}   list_all(P, x#xs) = (P(x) & list_all(P, xs))
 \end{ttbox}
 \caption{Rewrite rules for lists} \label{hol-list-simps}
 \end{figure}