removal of the (thm list) argument of mk_cases
authorpaulson
Tue Jan 19 11:18:11 1999 +0100 (1999-01-19)
changeset 6141a6922171b396
parent 6140 af32e2c3f77a
child 6142 c0c93b9434ef
removal of the (thm list) argument of mk_cases
NEWS
doc-src/Inductive/ind-defs.tex
doc-src/Logics/HOL.tex
doc-src/Logics/logics.ind
doc-src/ZF/ZF.tex
src/HOL/Auth/Message.ML
src/HOL/Finite.ML
src/HOL/IMP/Expr.ML
src/HOL/IMP/Natural.ML
src/HOL/IMP/Transition.ML
src/HOL/Induct/Com.ML
src/HOL/Induct/Comb.ML
src/HOL/Induct/Exp.ML
src/HOL/Induct/LFilter.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/InductTermi.ML
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/ParRed.ML
src/HOL/List.ML
src/HOL/List.thy
src/HOL/MiniML/W.ML
src/HOL/Tools/inductive_package.ML
src/HOL/W0/W.ML
src/ZF/Coind/ECR.ML
src/ZF/Coind/MT.ML
src/ZF/Coind/Static.ML
src/ZF/Coind/Static.thy
src/ZF/Coind/Types.ML
src/ZF/Datatype.ML
src/ZF/IMP/Com.ML
src/ZF/IMP/Equiv.ML
src/ZF/List.ML
src/ZF/Resid/Redex.ML
src/ZF/Resid/Reduction.ML
src/ZF/Resid/Residuals.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/ex/BT.ML
src/ZF/ex/CoUnit.ML
src/ZF/ex/Comb.ML
src/ZF/ex/Enum.ML
src/ZF/ex/LList.ML
src/ZF/ex/ListN.ML
src/ZF/ex/PropLog.ML
src/ZF/ex/Rmap.ML
     1.1 --- a/NEWS	Tue Jan 19 11:16:39 1999 +0100
     1.2 +++ b/NEWS	Tue Jan 19 11:18:11 1999 +0100
     1.3 @@ -11,6 +11,10 @@
     1.4  * ZF: The con_defs part of an inductive definition may no longer refer to 
     1.5    constants declared in the same theory;
     1.6  
     1.7 +* HOL, ZF: the function mk_cases, generated by the inductive definition 
     1.8 +  package, has lost an argument.  To simplify its result, it uses the default
     1.9 +  simpset instead of a supplied list of theorems.
    1.10 +
    1.11  
    1.12  *** Proof tools ***
    1.13  
    1.14 @@ -68,6 +72,9 @@
    1.15  
    1.16  * the datatype declaration of type T now defines the recursor T_rec;
    1.17  
    1.18 +* simplification automatically does freeness reasoning for datatype
    1.19 +  constructors;
    1.20 +
    1.21  * The syntax "if P then x else y" is now available in addition to if(P,x,y).
    1.22  
    1.23  
     2.1 --- a/doc-src/Inductive/ind-defs.tex	Tue Jan 19 11:16:39 1999 +0100
     2.2 +++ b/doc-src/Inductive/ind-defs.tex	Tue Jan 19 11:18:11 1999 +0100
     2.3 @@ -632,9 +632,9 @@
     2.4  deduces the corresponding form of~$i$;  this is called rule inversion.  
     2.5  Here is a sample session: 
     2.6  \begin{ttbox}
     2.7 -listn.mk_cases list.con_defs "<i,Nil> : listn(A)";
     2.8 +listn.mk_cases "<i,Nil> : listn(A)";
     2.9  {\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm}
    2.10 -listn.mk_cases list.con_defs "<i,Cons(a,l)> : listn(A)";
    2.11 +listn.mk_cases "<i,Cons(a,l)> : listn(A)";
    2.12  {\out "[| <?i, Cons(?a, ?l)> : listn(?A);}
    2.13  {\out     !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q }
    2.14  {\out  |] ==> ?Q" : thm}
     3.1 --- a/doc-src/Logics/HOL.tex	Tue Jan 19 11:16:39 1999 +0100
     3.2 +++ b/doc-src/Logics/HOL.tex	Tue Jan 19 11:18:11 1999 +0100
     3.3 @@ -2657,7 +2657,7 @@
     3.4  \item[\tt elim] is the head of the list \texttt{elims}.
     3.5    
     3.6  \item[\tt mk_cases] is a function to create simplified instances of {\tt
     3.7 -elim}, using freeness reasoning on some underlying datatype.
     3.8 +elim} using freeness reasoning on underlying datatypes.
     3.9  \end{description}
    3.10  
    3.11  For an inductive definition, the result structure contains the
    3.12 @@ -2676,7 +2676,7 @@
    3.13  val intrs        : thm list
    3.14  val elims        : thm list
    3.15  val elim         : thm
    3.16 -val mk_cases     : thm list -> string -> thm
    3.17 +val mk_cases     : string -> thm
    3.18  {\it(Inductive definitions only)} 
    3.19  val induct       : thm
    3.20  {\it(coinductive definitions only)}
     4.1 --- a/doc-src/Logics/logics.ind	Tue Jan 19 11:16:39 1999 +0100
     4.2 +++ b/doc-src/Logics/logics.ind	Tue Jan 19 11:18:11 1999 +0100
     4.3 @@ -1,652 +1,659 @@
     4.4  \begin{theindex}
     4.5  
     4.6 -  \item {\tt !} symbol, 2, 4, 11, 12, 24
     4.7 -  \item {\tt[]} symbol, 24
     4.8 -  \item {\tt\#} symbol, 24
     4.9 -  \item {\tt\#*} symbol, 80
    4.10 -  \item {\tt\#+} symbol, 80
    4.11 -  \item {\tt\&} symbol, 2, 56
    4.12 -  \item {\tt *} symbol, 3, 21, 71
    4.13 -  \item {\tt *} type, 19
    4.14 -  \item {\tt +} symbol, 3, 21, 71
    4.15 -  \item {\tt +} type, 19
    4.16 -  \item {\tt -} symbol, 3, 21, 80
    4.17 -  \item {\tt -->} symbol, 2, 56, 71
    4.18 -  \item {\tt :} symbol, 10
    4.19 -  \item {\tt <} constant, 22
    4.20 -  \item {\tt <} symbol, 21
    4.21 -  \item {\tt <->} symbol, 56
    4.22 -  \item {\tt <=} constant, 22
    4.23 -  \item {\tt <=} symbol, 10
    4.24 -  \item {\tt =} symbol, 2, 56, 71
    4.25 -  \item {\tt ?} symbol, 2, 4, 11, 12
    4.26 -  \item {\tt ?!} symbol, 2
    4.27 -  \item {\tt\at} symbol, 2, 24
    4.28 -  \item {\tt `} symbol, 71
    4.29 -  \item {\tt ``} symbol, 10
    4.30 -  \item \verb'{}' symbol, 10
    4.31 -  \item {\tt |} symbol, 2, 56
    4.32 -  \item {\tt |-|} symbol, 80
    4.33 +  \item {\tt !} symbol, 6, 8, 15, 16, 28
    4.34 +  \item {\tt[]} symbol, 28
    4.35 +  \item {\tt\#} symbol, 28
    4.36 +  \item {\tt\#*} symbol, 83
    4.37 +  \item {\tt\#+} symbol, 83
    4.38 +  \item {\tt\&} symbol, 6, 59
    4.39 +  \item {\tt *} symbol, 7, 25, 74
    4.40 +  \item {\tt *} type, 23
    4.41 +  \item {\tt +} symbol, 7, 25, 74
    4.42 +  \item {\tt +} type, 23
    4.43 +  \item {\tt -} symbol, 7, 25, 83
    4.44 +  \item {\tt -->} symbol, 6, 59, 74
    4.45 +  \item {\tt :} symbol, 14
    4.46 +  \item {\tt <} constant, 26
    4.47 +  \item {\tt <} symbol, 25
    4.48 +  \item {\tt <->} symbol, 59
    4.49 +  \item {\tt <=} constant, 26
    4.50 +  \item {\tt <=} symbol, 14
    4.51 +  \item {\tt =} symbol, 6, 59, 74
    4.52 +  \item {\tt ?} symbol, 6, 8, 15, 16
    4.53 +  \item {\tt ?!} symbol, 6
    4.54 +  \item {\tt\at} symbol, 6, 28
    4.55 +  \item {\tt `} symbol, 74
    4.56 +  \item {\tt ``} symbol, 14
    4.57 +  \item \verb'{}' symbol, 14
    4.58 +  \item {\tt |} symbol, 6, 59
    4.59 +  \item {\tt |-|} symbol, 83
    4.60  
    4.61    \indexspace
    4.62  
    4.63 -  \item {\tt 0} constant, 21, 69
    4.64 +  \item {\tt 0} constant, 25, 72
    4.65  
    4.66    \indexspace
    4.67  
    4.68 -  \item {\tt absdiff_def} theorem, 80
    4.69 -  \item {\tt add_assoc} theorem, 80
    4.70 -  \item {\tt add_commute} theorem, 80
    4.71 -  \item {\tt add_def} theorem, 80
    4.72 -  \item {\tt add_inverse_diff} theorem, 80
    4.73 -  \item {\tt add_mp_tac}, \bold{78}
    4.74 -  \item {\tt add_mult_dist} theorem, 80
    4.75 -  \item {\tt add_safes}, \bold{62}
    4.76 -  \item {\tt add_typing} theorem, 80
    4.77 -  \item {\tt add_unsafes}, \bold{62}
    4.78 -  \item {\tt addC0} theorem, 80
    4.79 -  \item {\tt addC_succ} theorem, 80
    4.80 -  \item {\tt Addsplits}, \bold{18}
    4.81 -  \item {\tt addsplits}, \bold{18}, 23, 35
    4.82 -  \item {\tt ALL} symbol, 2, 4, 11, 12, 56
    4.83 -  \item {\tt All} constant, 2, 56
    4.84 -  \item {\tt All_def} theorem, 6
    4.85 -  \item {\tt all_dupE} theorem, 8
    4.86 -  \item {\tt allE} theorem, 8
    4.87 -  \item {\tt allI} theorem, 8
    4.88 -  \item {\tt allL} theorem, 58, 62
    4.89 -  \item {\tt allL_thin} theorem, 59
    4.90 -  \item {\tt allR} theorem, 58
    4.91 -  \item {\tt and_def} theorem, 6
    4.92 -  \item {\tt arg_cong} theorem, 7
    4.93 -  \item {\tt Arith} theory, 22, 79
    4.94 +  \item {\tt absdiff_def} theorem, 83
    4.95 +  \item {\tt add_assoc} theorem, 83
    4.96 +  \item {\tt add_commute} theorem, 83
    4.97 +  \item {\tt add_def} theorem, 83
    4.98 +  \item {\tt add_inverse_diff} theorem, 83
    4.99 +  \item {\tt add_mp_tac}, \bold{81}
   4.100 +  \item {\tt add_mult_dist} theorem, 83
   4.101 +  \item {\tt add_safes}, \bold{65}
   4.102 +  \item {\tt add_typing} theorem, 83
   4.103 +  \item {\tt add_unsafes}, \bold{65}
   4.104 +  \item {\tt addC0} theorem, 83
   4.105 +  \item {\tt addC_succ} theorem, 83
   4.106 +  \item {\tt Addsplits}, \bold{22}
   4.107 +  \item {\tt addsplits}, \bold{22}, 27, 39
   4.108 +  \item {\tt ALL} symbol, 6, 8, 15, 16, 59
   4.109 +  \item {\tt All} constant, 6, 59
   4.110 +  \item {\tt All_def} theorem, 10
   4.111 +  \item {\tt all_dupE} theorem, 12
   4.112 +  \item {\tt allE} theorem, 12
   4.113 +  \item {\tt allI} theorem, 12
   4.114 +  \item {\tt allL} theorem, 61, 65
   4.115 +  \item {\tt allL_thin} theorem, 62
   4.116 +  \item {\tt allR} theorem, 61
   4.117 +  \item {\tt and_def} theorem, 10
   4.118 +  \item {\tt arg_cong} theorem, 11
   4.119 +  \item {\tt Arith} theory, 26, 82
   4.120    \item assumptions
   4.121 -    \subitem in {\CTT}, 68, 78
   4.122 +    \subitem in {\CTT}, 71, 81
   4.123  
   4.124    \indexspace
   4.125  
   4.126 -  \item {\tt Ball} constant, 10, 12
   4.127 -  \item {\tt Ball_def} theorem, 13
   4.128 -  \item {\tt ballE} theorem, 14
   4.129 -  \item {\tt ballI} theorem, 14
   4.130 -  \item {\tt basic} theorem, 58
   4.131 -  \item {\tt basic_defs}, \bold{76}
   4.132 -  \item {\tt best_tac}, \bold{63}
   4.133 -  \item {\tt Bex} constant, 10, 12
   4.134 -  \item {\tt Bex_def} theorem, 13
   4.135 -  \item {\tt bexCI} theorem, 12, 14
   4.136 -  \item {\tt bexE} theorem, 14
   4.137 -  \item {\tt bexI} theorem, 12, 14
   4.138 -  \item {\textit {bool}} type, 3
   4.139 -  \item {\tt box_equals} theorem, 7, 9
   4.140 -  \item {\tt bspec} theorem, 14
   4.141 -  \item {\tt butlast} constant, 24
   4.142 +  \item {\tt Ball} constant, 14, 16
   4.143 +  \item {\tt Ball_def} theorem, 17
   4.144 +  \item {\tt ballE} theorem, 18
   4.145 +  \item {\tt ballI} theorem, 18
   4.146 +  \item {\tt basic} theorem, 61
   4.147 +  \item {\tt basic_defs}, \bold{79}
   4.148 +  \item {\tt best_tac}, \bold{66}
   4.149 +  \item {\tt Bex} constant, 14, 16
   4.150 +  \item {\tt Bex_def} theorem, 17
   4.151 +  \item {\tt bexCI} theorem, 16, 18
   4.152 +  \item {\tt bexE} theorem, 18
   4.153 +  \item {\tt bexI} theorem, 16, 18
   4.154 +  \item {\textit {bool}} type, 7
   4.155 +  \item {\tt box_equals} theorem, 11, 13
   4.156 +  \item {\tt bspec} theorem, 18
   4.157 +  \item {\tt butlast} constant, 28
   4.158  
   4.159    \indexspace
   4.160  
   4.161 -  \item {\tt case} symbol, 5, 22, 23, 35
   4.162 -  \item {\tt case_tac}, \bold{9}
   4.163 -  \item {\tt ccontr} theorem, 8
   4.164 -  \item {\tt classical} theorem, 8
   4.165 -  \item {\tt coinductive}, 47--50
   4.166 -  \item {\tt Collect} constant, 10, 12
   4.167 -  \item {\tt Collect_mem_eq} theorem, 12, 13
   4.168 -  \item {\tt CollectD} theorem, 14, 53
   4.169 -  \item {\tt CollectE} theorem, 14
   4.170 -  \item {\tt CollectI} theorem, 14, 53
   4.171 -  \item {\tt comp_rls}, \bold{76}
   4.172 -  \item {\tt Compl} constant, 10
   4.173 -  \item {\tt Compl_def} theorem, 13
   4.174 -  \item {\tt Compl_disjoint} theorem, 16
   4.175 -  \item {\tt Compl_Int} theorem, 16
   4.176 -  \item {\tt Compl_partition} theorem, 16
   4.177 -  \item {\tt Compl_Un} theorem, 16
   4.178 -  \item {\tt ComplD} theorem, 15
   4.179 -  \item {\tt ComplI} theorem, 15
   4.180 -  \item {\tt concat} constant, 24
   4.181 -  \item {\tt cong} theorem, 7
   4.182 -  \item {\tt conj_cong}, 17
   4.183 -  \item {\tt conjE} theorem, 7
   4.184 -  \item {\tt conjI} theorem, 7
   4.185 -  \item {\tt conjL} theorem, 58
   4.186 -  \item {\tt conjR} theorem, 58
   4.187 -  \item {\tt conjunct1} theorem, 7
   4.188 -  \item {\tt conjunct2} theorem, 7
   4.189 -  \item {\tt conL} theorem, 59
   4.190 -  \item {\tt conR} theorem, 59
   4.191 -  \item Constructive Type Theory, 68--90
   4.192 -  \item {\tt contr} constant, 69
   4.193 -  \item {\tt could_res}, \bold{61}
   4.194 -  \item {\tt could_resolve_seq}, \bold{61}
   4.195 -  \item {\tt CTT} theory, 68
   4.196 -  \item {\tt cut} theorem, 58
   4.197 -  \item {\tt cutL_tac}, \bold{60}
   4.198 -  \item {\tt cutR_tac}, \bold{60}
   4.199 +  \item {\tt case} symbol, 9, 26, 27, 39
   4.200 +  \item {\tt case_tac}, \bold{13}
   4.201 +  \item {\tt CCL} theory, 1
   4.202 +  \item {\tt ccontr} theorem, 12
   4.203 +  \item {\tt classical} theorem, 12
   4.204 +  \item {\tt coinductive}, 51--53
   4.205 +  \item {\tt Collect} constant, 14, 16
   4.206 +  \item {\tt Collect_mem_eq} theorem, 16, 17
   4.207 +  \item {\tt CollectD} theorem, 18, 56
   4.208 +  \item {\tt CollectE} theorem, 18
   4.209 +  \item {\tt CollectI} theorem, 18, 57
   4.210 +  \item {\tt comp_rls}, \bold{79}
   4.211 +  \item {\tt Compl} constant, 14
   4.212 +  \item {\tt Compl_def} theorem, 17
   4.213 +  \item {\tt Compl_disjoint} theorem, 20
   4.214 +  \item {\tt Compl_Int} theorem, 20
   4.215 +  \item {\tt Compl_partition} theorem, 20
   4.216 +  \item {\tt Compl_Un} theorem, 20
   4.217 +  \item {\tt ComplD} theorem, 19
   4.218 +  \item {\tt ComplI} theorem, 19
   4.219 +  \item {\tt concat} constant, 28
   4.220 +  \item {\tt cong} theorem, 11
   4.221 +  \item {\tt conj_cong}, 21
   4.222 +  \item {\tt conjE} theorem, 11
   4.223 +  \item {\tt conjI} theorem, 11
   4.224 +  \item {\tt conjL} theorem, 61
   4.225 +  \item {\tt conjR} theorem, 61
   4.226 +  \item {\tt conjunct1} theorem, 11
   4.227 +  \item {\tt conjunct2} theorem, 11
   4.228 +  \item {\tt conL} theorem, 62
   4.229 +  \item {\tt conR} theorem, 62
   4.230 +  \item Constructive Type Theory, 71--93
   4.231 +  \item {\tt contr} constant, 72
   4.232 +  \item {\tt could_res}, \bold{64}
   4.233 +  \item {\tt could_resolve_seq}, \bold{64}
   4.234 +  \item {\tt CTT} theory, 1, 71
   4.235 +  \item {\tt Cube} theory, 1
   4.236 +  \item {\tt cut} theorem, 61
   4.237 +  \item {\tt cutL_tac}, \bold{63}
   4.238 +  \item {\tt cutR_tac}, \bold{63}
   4.239  
   4.240    \indexspace
   4.241  
   4.242 -  \item {\tt datatype}, 32--40
   4.243 -  \item {\tt Delsplits}, \bold{18}
   4.244 -  \item {\tt delsplits}, \bold{18}
   4.245 -  \item {\tt diff_0_eq_0} theorem, 80
   4.246 -  \item {\tt diff_def} theorem, 80
   4.247 -  \item {\tt diff_self_eq_0} theorem, 80
   4.248 -  \item {\tt diff_succ_succ} theorem, 80
   4.249 -  \item {\tt diff_typing} theorem, 80
   4.250 -  \item {\tt diffC0} theorem, 80
   4.251 -  \item {\tt disjCI} theorem, 8
   4.252 -  \item {\tt disjE} theorem, 7
   4.253 -  \item {\tt disjI1} theorem, 7
   4.254 -  \item {\tt disjI2} theorem, 7
   4.255 -  \item {\tt disjL} theorem, 58
   4.256 -  \item {\tt disjR} theorem, 58
   4.257 -  \item {\tt div} symbol, 21, 80
   4.258 -  \item {\tt div_def} theorem, 80
   4.259 -  \item {\tt div_geq} theorem, 22
   4.260 -  \item {\tt div_less} theorem, 22
   4.261 -  \item {\tt Divides} theory, 22
   4.262 -  \item {\tt double_complement} theorem, 16
   4.263 -  \item {\tt drop} constant, 24
   4.264 -  \item {\tt dropWhile} constant, 24
   4.265 +  \item {\tt datatype}, 36--44
   4.266 +  \item {\tt Delsplits}, \bold{22}
   4.267 +  \item {\tt delsplits}, \bold{22}
   4.268 +  \item {\tt diff_0_eq_0} theorem, 83
   4.269 +  \item {\tt diff_def} theorem, 83
   4.270 +  \item {\tt diff_self_eq_0} theorem, 83
   4.271 +  \item {\tt diff_succ_succ} theorem, 83
   4.272 +  \item {\tt diff_typing} theorem, 83
   4.273 +  \item {\tt diffC0} theorem, 83
   4.274 +  \item {\tt disjCI} theorem, 12
   4.275 +  \item {\tt disjE} theorem, 11
   4.276 +  \item {\tt disjI1} theorem, 11
   4.277 +  \item {\tt disjI2} theorem, 11
   4.278 +  \item {\tt disjL} theorem, 61
   4.279 +  \item {\tt disjR} theorem, 61
   4.280 +  \item {\tt div} symbol, 25, 83
   4.281 +  \item {\tt div_def} theorem, 83
   4.282 +  \item {\tt div_geq} theorem, 26
   4.283 +  \item {\tt div_less} theorem, 26
   4.284 +  \item {\tt Divides} theory, 26
   4.285 +  \item {\tt double_complement} theorem, 20
   4.286 +  \item {\tt drop} constant, 28
   4.287 +  \item {\tt dropWhile} constant, 28
   4.288  
   4.289    \indexspace
   4.290  
   4.291 -  \item {\tt Elem} constant, 69
   4.292 -  \item {\tt elim_rls}, \bold{76}
   4.293 -  \item {\tt elimL_rls}, \bold{76}
   4.294 -  \item {\tt empty_def} theorem, 13
   4.295 -  \item {\tt empty_pack}, \bold{62}
   4.296 -  \item {\tt emptyE} theorem, 15
   4.297 -  \item {\tt Eps} constant, 2, 4
   4.298 -  \item {\tt Eq} constant, 69
   4.299 -  \item {\tt eq} constant, 69, 74
   4.300 -  \item {\tt EqC} theorem, 75
   4.301 -  \item {\tt EqE} theorem, 75
   4.302 -  \item {\tt Eqelem} constant, 69
   4.303 -  \item {\tt EqF} theorem, 75
   4.304 -  \item {\tt EqFL} theorem, 75
   4.305 -  \item {\tt EqI} theorem, 75
   4.306 -  \item {\tt Eqtype} constant, 69
   4.307 -  \item {\tt equal_tac}, \bold{77}
   4.308 -  \item {\tt equal_types} theorem, 72
   4.309 -  \item {\tt equal_typesL} theorem, 72
   4.310 -  \item {\tt equalityCE} theorem, 12, 14, 53, 54
   4.311 -  \item {\tt equalityD1} theorem, 14
   4.312 -  \item {\tt equalityD2} theorem, 14
   4.313 -  \item {\tt equalityE} theorem, 14
   4.314 -  \item {\tt equalityI} theorem, 14
   4.315 -  \item {\tt EX} symbol, 2, 4, 11, 12, 56
   4.316 -  \item {\tt Ex} constant, 2, 56
   4.317 -  \item {\tt EX!} symbol, 2
   4.318 -  \item {\tt Ex1} constant, 2
   4.319 -  \item {\tt Ex1_def} theorem, 6
   4.320 -  \item {\tt ex1E} theorem, 8
   4.321 -  \item {\tt ex1I} theorem, 8
   4.322 -  \item {\tt Ex_def} theorem, 6
   4.323 -  \item {\tt exCI} theorem, 8
   4.324 -  \item {\tt excluded_middle} theorem, 8
   4.325 -  \item {\tt exE} theorem, 8
   4.326 -  \item {\tt exhaust_tac}, \bold{36}
   4.327 -  \item {\tt exI} theorem, 8
   4.328 -  \item {\tt exL} theorem, 58
   4.329 -  \item {\tt Exp} theory, 51
   4.330 -  \item {\tt exR} theorem, 58, 62, 64
   4.331 -  \item {\tt exR_thin} theorem, 59, 64, 65
   4.332 -  \item {\tt ext} theorem, 5, 6
   4.333 +  \item {\tt Elem} constant, 72
   4.334 +  \item {\tt elim_rls}, \bold{79}
   4.335 +  \item {\tt elimL_rls}, \bold{79}
   4.336 +  \item {\tt empty_def} theorem, 17
   4.337 +  \item {\tt empty_pack}, \bold{65}
   4.338 +  \item {\tt emptyE} theorem, 19
   4.339 +  \item {\tt Eps} constant, 6, 8
   4.340 +  \item {\tt Eq} constant, 72
   4.341 +  \item {\tt eq} constant, 72, 77
   4.342 +  \item {\tt EqC} theorem, 78
   4.343 +  \item {\tt EqE} theorem, 78
   4.344 +  \item {\tt Eqelem} constant, 72
   4.345 +  \item {\tt EqF} theorem, 78
   4.346 +  \item {\tt EqFL} theorem, 78
   4.347 +  \item {\tt EqI} theorem, 78
   4.348 +  \item {\tt Eqtype} constant, 72
   4.349 +  \item {\tt equal_tac}, \bold{80}
   4.350 +  \item {\tt equal_types} theorem, 75
   4.351 +  \item {\tt equal_typesL} theorem, 75
   4.352 +  \item {\tt equalityCE} theorem, 16, 18, 56, 57
   4.353 +  \item {\tt equalityD1} theorem, 18
   4.354 +  \item {\tt equalityD2} theorem, 18
   4.355 +  \item {\tt equalityE} theorem, 18
   4.356 +  \item {\tt equalityI} theorem, 18
   4.357 +  \item {\tt EX} symbol, 6, 8, 15, 16, 59
   4.358 +  \item {\tt Ex} constant, 6, 59
   4.359 +  \item {\tt EX!} symbol, 6
   4.360 +  \item {\tt Ex1} constant, 6
   4.361 +  \item {\tt Ex1_def} theorem, 10
   4.362 +  \item {\tt ex1E} theorem, 12
   4.363 +  \item {\tt ex1I} theorem, 12
   4.364 +  \item {\tt Ex_def} theorem, 10
   4.365 +  \item {\tt exCI} theorem, 12
   4.366 +  \item {\tt excluded_middle} theorem, 12
   4.367 +  \item {\tt exE} theorem, 12
   4.368 +  \item {\tt exhaust_tac}, \bold{40}
   4.369 +  \item {\tt exI} theorem, 12
   4.370 +  \item {\tt exL} theorem, 61
   4.371 +  \item {\tt Exp} theory, 55
   4.372 +  \item {\tt exR} theorem, 61, 65, 67
   4.373 +  \item {\tt exR_thin} theorem, 62, 67, 68
   4.374 +  \item {\tt ext} theorem, 9, 10
   4.375  
   4.376    \indexspace
   4.377  
   4.378 -  \item {\tt F} constant, 69
   4.379 -  \item {\tt False} constant, 2, 56
   4.380 -  \item {\tt False_def} theorem, 6
   4.381 -  \item {\tt FalseE} theorem, 7
   4.382 -  \item {\tt FalseL} theorem, 58
   4.383 -  \item {\tt fast_tac}, \bold{63}
   4.384 -  \item {\tt FE} theorem, 75, 79
   4.385 -  \item {\tt FEL} theorem, 75
   4.386 -  \item {\tt FF} theorem, 75
   4.387 -  \item {\tt filseq_resolve_tac}, \bold{61}
   4.388 -  \item {\tt filt_resolve_tac}, 61, 77
   4.389 -  \item {\tt filter} constant, 24
   4.390 -  \item flex-flex constraints, 57
   4.391 -  \item {\tt FOL} theory, 78
   4.392 -  \item {\tt foldl} constant, 24
   4.393 -  \item {\tt form_rls}, \bold{76}
   4.394 -  \item {\tt formL_rls}, \bold{76}
   4.395 -  \item {\tt forms_of_seq}, \bold{60}
   4.396 -  \item {\tt fst} constant, 19, 69, 74
   4.397 -  \item {\tt fst_conv} theorem, 19
   4.398 -  \item {\tt fst_def} theorem, 74
   4.399 -  \item {\tt Fun} theory, 17
   4.400 -  \item {\textit {fun}} type, 3
   4.401 -  \item {\tt fun_cong} theorem, 7
   4.402 +  \item {\tt F} constant, 72
   4.403 +  \item {\tt False} constant, 6, 59
   4.404 +  \item {\tt False_def} theorem, 10
   4.405 +  \item {\tt FalseE} theorem, 11
   4.406 +  \item {\tt FalseL} theorem, 61
   4.407 +  \item {\tt fast_tac}, \bold{66}
   4.408 +  \item {\tt FE} theorem, 78, 82
   4.409 +  \item {\tt FEL} theorem, 78
   4.410 +  \item {\tt FF} theorem, 78
   4.411 +  \item {\tt filseq_resolve_tac}, \bold{64}
   4.412 +  \item {\tt filt_resolve_tac}, 64, 80
   4.413 +  \item {\tt filter} constant, 28
   4.414 +  \item flex-flex constraints, 60
   4.415 +  \item {\tt FOL} theory, 81
   4.416 +  \item {\tt foldl} constant, 28
   4.417 +  \item {\tt form_rls}, \bold{79}
   4.418 +  \item {\tt formL_rls}, \bold{79}
   4.419 +  \item {\tt forms_of_seq}, \bold{63}
   4.420 +  \item {\tt fst} constant, 23, 72, 77
   4.421 +  \item {\tt fst_conv} theorem, 23
   4.422 +  \item {\tt fst_def} theorem, 77
   4.423 +  \item {\tt Fun} theory, 21
   4.424 +  \item {\textit {fun}} type, 7
   4.425 +  \item {\tt fun_cong} theorem, 11
   4.426    \item function applications
   4.427 -    \subitem in \CTT, 71
   4.428 +    \subitem in \CTT, 74
   4.429  
   4.430    \indexspace
   4.431  
   4.432 -  \item {\tt hd} constant, 24
   4.433 -  \item higher-order logic, 1--54
   4.434 -  \item {\tt HOL} theory, 1
   4.435 -  \item {\sc hol} system, 1, 4
   4.436 -  \item {\tt HOL_basic_ss}, \bold{17}
   4.437 -  \item {\tt HOL_cs}, \bold{18}
   4.438 -  \item {\tt HOL_quantifiers}, \bold{4}, 12
   4.439 -  \item {\tt HOL_ss}, \bold{17}
   4.440 -  \item {\tt hyp_rew_tac}, \bold{78}
   4.441 -  \item {\tt hyp_subst_tac}, 17
   4.442 +  \item {\tt hd} constant, 28
   4.443 +  \item higher-order logic, 5--57
   4.444 +  \item {\tt HOL} theory, 1, 5
   4.445 +  \item {\sc hol} system, 5, 8
   4.446 +  \item {\tt HOL_basic_ss}, \bold{21}
   4.447 +  \item {\tt HOL_cs}, \bold{22}
   4.448 +  \item {\tt HOL_quantifiers}, \bold{8}, 16
   4.449 +  \item {\tt HOL_ss}, \bold{21}
   4.450 +  \item {\tt HOLCF} theory, 1
   4.451 +  \item {\tt hyp_rew_tac}, \bold{81}
   4.452 +  \item {\tt hyp_subst_tac}, 21
   4.453  
   4.454    \indexspace
   4.455  
   4.456 -  \item {\textit {i}} type, 68
   4.457 -  \item {\tt If} constant, 2
   4.458 -  \item {\tt if_def} theorem, 6
   4.459 -  \item {\tt if_not_P} theorem, 8
   4.460 -  \item {\tt if_P} theorem, 8
   4.461 -  \item {\tt iff} theorem, 5, 6
   4.462 -  \item {\tt iff_def} theorem, 58
   4.463 -  \item {\tt iffCE} theorem, 8, 12
   4.464 -  \item {\tt iffD1} theorem, 7
   4.465 -  \item {\tt iffD2} theorem, 7
   4.466 -  \item {\tt iffE} theorem, 7
   4.467 -  \item {\tt iffI} theorem, 7
   4.468 -  \item {\tt iffL} theorem, 59, 66
   4.469 -  \item {\tt iffR} theorem, 59
   4.470 -  \item {\tt image_def} theorem, 13
   4.471 -  \item {\tt imageE} theorem, 15
   4.472 -  \item {\tt imageI} theorem, 15
   4.473 -  \item {\tt impCE} theorem, 8
   4.474 -  \item {\tt impE} theorem, 7
   4.475 -  \item {\tt impI} theorem, 5
   4.476 -  \item {\tt impL} theorem, 58
   4.477 -  \item {\tt impR} theorem, 58
   4.478 -  \item {\tt in} symbol, 3
   4.479 -  \item {\textit {ind}} type, 20
   4.480 -  \item {\tt induct_tac}, 22, \bold{36}
   4.481 -  \item {\tt inductive}, 47--50
   4.482 -  \item {\tt inj} constant, 17
   4.483 -  \item {\tt inj_def} theorem, 17
   4.484 -  \item {\tt inj_Inl} theorem, 21
   4.485 -  \item {\tt inj_Inr} theorem, 21
   4.486 -  \item {\tt inj_on} constant, 17
   4.487 -  \item {\tt inj_on_def} theorem, 17
   4.488 -  \item {\tt inj_Suc} theorem, 21
   4.489 -  \item {\tt Inl} constant, 21
   4.490 -  \item {\tt inl} constant, 69, 74, 84
   4.491 -  \item {\tt Inl_not_Inr} theorem, 21
   4.492 -  \item {\tt Inr} constant, 21
   4.493 -  \item {\tt inr} constant, 69, 74
   4.494 -  \item {\tt insert} constant, 10
   4.495 -  \item {\tt insert_def} theorem, 13
   4.496 -  \item {\tt insertE} theorem, 15
   4.497 -  \item {\tt insertI1} theorem, 15
   4.498 -  \item {\tt insertI2} theorem, 15
   4.499 -  \item {\tt INT} symbol, 10--12
   4.500 -  \item {\tt Int} symbol, 10
   4.501 -  \item {\tt Int_absorb} theorem, 16
   4.502 -  \item {\tt Int_assoc} theorem, 16
   4.503 -  \item {\tt Int_commute} theorem, 16
   4.504 -  \item {\tt INT_D} theorem, 15
   4.505 -  \item {\tt Int_def} theorem, 13
   4.506 -  \item {\tt INT_E} theorem, 15
   4.507 -  \item {\tt Int_greatest} theorem, 16
   4.508 -  \item {\tt INT_I} theorem, 15
   4.509 -  \item {\tt Int_Inter_image} theorem, 16
   4.510 -  \item {\tt Int_lower1} theorem, 16
   4.511 -  \item {\tt Int_lower2} theorem, 16
   4.512 -  \item {\tt Int_Un_distrib} theorem, 16
   4.513 -  \item {\tt Int_Union} theorem, 16
   4.514 -  \item {\tt IntD1} theorem, 15
   4.515 -  \item {\tt IntD2} theorem, 15
   4.516 -  \item {\tt IntE} theorem, 15
   4.517 -  \item {\tt INTER} constant, 10
   4.518 -  \item {\tt Inter} constant, 10
   4.519 -  \item {\tt INTER1} constant, 10
   4.520 -  \item {\tt INTER1_def} theorem, 13
   4.521 -  \item {\tt INTER_def} theorem, 13
   4.522 -  \item {\tt Inter_def} theorem, 13
   4.523 -  \item {\tt Inter_greatest} theorem, 16
   4.524 -  \item {\tt Inter_lower} theorem, 16
   4.525 -  \item {\tt Inter_Un_distrib} theorem, 16
   4.526 -  \item {\tt InterD} theorem, 15
   4.527 -  \item {\tt InterE} theorem, 15
   4.528 -  \item {\tt InterI} theorem, 15
   4.529 -  \item {\tt IntI} theorem, 15
   4.530 -  \item {\tt intr_rls}, \bold{76}
   4.531 -  \item {\tt intr_tac}, \bold{77}, 86, 87
   4.532 -  \item {\tt intrL_rls}, \bold{76}
   4.533 -  \item {\tt inv} constant, 17
   4.534 -  \item {\tt inv_def} theorem, 17
   4.535 +  \item {\textit {i}} type, 71
   4.536 +  \item {\tt If} constant, 6
   4.537 +  \item {\tt if_def} theorem, 10
   4.538 +  \item {\tt if_not_P} theorem, 12
   4.539 +  \item {\tt if_P} theorem, 12
   4.540 +  \item {\tt iff} theorem, 9, 10
   4.541 +  \item {\tt iff_def} theorem, 61
   4.542 +  \item {\tt iffCE} theorem, 12, 16
   4.543 +  \item {\tt iffD1} theorem, 11
   4.544 +  \item {\tt iffD2} theorem, 11
   4.545 +  \item {\tt iffE} theorem, 11
   4.546 +  \item {\tt iffI} theorem, 11
   4.547 +  \item {\tt iffL} theorem, 62, 69
   4.548 +  \item {\tt iffR} theorem, 62
   4.549 +  \item {\tt ILL} theory, 1
   4.550 +  \item {\tt image_def} theorem, 17
   4.551 +  \item {\tt imageE} theorem, 19
   4.552 +  \item {\tt imageI} theorem, 19
   4.553 +  \item {\tt impCE} theorem, 12
   4.554 +  \item {\tt impE} theorem, 11
   4.555 +  \item {\tt impI} theorem, 9
   4.556 +  \item {\tt impL} theorem, 61
   4.557 +  \item {\tt impR} theorem, 61
   4.558 +  \item {\tt in} symbol, 7
   4.559 +  \item {\textit {ind}} type, 24
   4.560 +  \item {\tt induct_tac}, 26, \bold{40}
   4.561 +  \item {\tt inductive}, 51--53
   4.562 +  \item {\tt inj} constant, 21
   4.563 +  \item {\tt inj_def} theorem, 21
   4.564 +  \item {\tt inj_Inl} theorem, 25
   4.565 +  \item {\tt inj_Inr} theorem, 25
   4.566 +  \item {\tt inj_on} constant, 21
   4.567 +  \item {\tt inj_on_def} theorem, 21
   4.568 +  \item {\tt inj_Suc} theorem, 25
   4.569 +  \item {\tt Inl} constant, 25
   4.570 +  \item {\tt inl} constant, 72, 77, 87
   4.571 +  \item {\tt Inl_not_Inr} theorem, 25
   4.572 +  \item {\tt Inr} constant, 25
   4.573 +  \item {\tt inr} constant, 72, 77
   4.574 +  \item {\tt insert} constant, 14
   4.575 +  \item {\tt insert_def} theorem, 17
   4.576 +  \item {\tt insertE} theorem, 19
   4.577 +  \item {\tt insertI1} theorem, 19
   4.578 +  \item {\tt insertI2} theorem, 19
   4.579 +  \item {\tt INT} symbol, 14--16
   4.580 +  \item {\tt Int} symbol, 14
   4.581 +  \item {\tt Int_absorb} theorem, 20
   4.582 +  \item {\tt Int_assoc} theorem, 20
   4.583 +  \item {\tt Int_commute} theorem, 20
   4.584 +  \item {\tt INT_D} theorem, 19
   4.585 +  \item {\tt Int_def} theorem, 17
   4.586 +  \item {\tt INT_E} theorem, 19
   4.587 +  \item {\tt Int_greatest} theorem, 20
   4.588 +  \item {\tt INT_I} theorem, 19
   4.589 +  \item {\tt Int_Inter_image} theorem, 20
   4.590 +  \item {\tt Int_lower1} theorem, 20
   4.591 +  \item {\tt Int_lower2} theorem, 20
   4.592 +  \item {\tt Int_Un_distrib} theorem, 20
   4.593 +  \item {\tt Int_Union} theorem, 20
   4.594 +  \item {\tt IntD1} theorem, 19
   4.595 +  \item {\tt IntD2} theorem, 19
   4.596 +  \item {\tt IntE} theorem, 19
   4.597 +  \item {\tt INTER} constant, 14
   4.598 +  \item {\tt Inter} constant, 14
   4.599 +  \item {\tt INTER1} constant, 14
   4.600 +  \item {\tt INTER1_def} theorem, 17
   4.601 +  \item {\tt INTER_def} theorem, 17
   4.602 +  \item {\tt Inter_def} theorem, 17
   4.603 +  \item {\tt Inter_greatest} theorem, 20
   4.604 +  \item {\tt Inter_lower} theorem, 20
   4.605 +  \item {\tt Inter_Un_distrib} theorem, 20
   4.606 +  \item {\tt InterD} theorem, 19
   4.607 +  \item {\tt InterE} theorem, 19
   4.608 +  \item {\tt InterI} theorem, 19
   4.609 +  \item {\tt IntI} theorem, 19
   4.610 +  \item {\tt intr_rls}, \bold{79}
   4.611 +  \item {\tt intr_tac}, \bold{80}, 89, 90
   4.612 +  \item {\tt intrL_rls}, \bold{79}
   4.613 +  \item {\tt inv} constant, 21
   4.614 +  \item {\tt inv_def} theorem, 21
   4.615  
   4.616    \indexspace
   4.617  
   4.618 -  \item {\tt lam} symbol, 71
   4.619 -  \item {\tt lambda} constant, 69, 71
   4.620 +  \item {\tt lam} symbol, 74
   4.621 +  \item {\tt lambda} constant, 72, 74
   4.622    \item $\lambda$-abstractions
   4.623 -    \subitem in \CTT, 71
   4.624 -  \item {\tt last} constant, 24
   4.625 -  \item {\tt LEAST} constant, 3, 4, 22
   4.626 -  \item {\tt Least} constant, 2
   4.627 -  \item {\tt Least_def} theorem, 6
   4.628 -  \item {\tt length} constant, 24
   4.629 -  \item {\tt less_induct} theorem, 23
   4.630 -  \item {\tt Let} constant, 2, 5
   4.631 -  \item {\tt let} symbol, 3, 5
   4.632 -  \item {\tt Let_def} theorem, 5, 6
   4.633 -  \item {\tt LFilter} theory, 51
   4.634 -  \item {\tt List} theory, 23, 24
   4.635 -  \item {\textit{list}} type, 23
   4.636 -  \item {\tt LK} theory, 55, 59
   4.637 -  \item {\tt LK_dup_pack}, \bold{62}, 63
   4.638 -  \item {\tt LK_pack}, \bold{62}
   4.639 -  \item {\tt LList} theory, 51
   4.640 +    \subitem in \CTT, 74
   4.641 +  \item {\tt last} constant, 28
   4.642 +  \item {\tt LCF} theory, 1
   4.643 +  \item {\tt LEAST} constant, 7, 8, 26
   4.644 +  \item {\tt Least} constant, 6
   4.645 +  \item {\tt Least_def} theorem, 10
   4.646 +  \item {\tt length} constant, 28
   4.647 +  \item {\tt less_induct} theorem, 27
   4.648 +  \item {\tt Let} constant, 6, 9
   4.649 +  \item {\tt let} symbol, 7, 9
   4.650 +  \item {\tt Let_def} theorem, 9, 10
   4.651 +  \item {\tt LFilter} theory, 55
   4.652 +  \item {\tt List} theory, 27, 28
   4.653 +  \item {\textit{list}} type, 27
   4.654 +  \item {\tt LK} theory, 1, 58, 62
   4.655 +  \item {\tt LK_dup_pack}, \bold{65}, 66
   4.656 +  \item {\tt LK_pack}, \bold{65}
   4.657 +  \item {\tt LList} theory, 54
   4.658  
   4.659    \indexspace
   4.660  
   4.661 -  \item {\tt map} constant, 24
   4.662 -  \item {\tt max} constant, 3, 22
   4.663 -  \item {\tt mem} symbol, 24
   4.664 -  \item {\tt mem_Collect_eq} theorem, 12, 13
   4.665 -  \item {\tt min} constant, 3, 22
   4.666 -  \item {\tt minus} class, 3
   4.667 -  \item {\tt mod} symbol, 21, 80
   4.668 -  \item {\tt mod_def} theorem, 80
   4.669 -  \item {\tt mod_geq} theorem, 22
   4.670 -  \item {\tt mod_less} theorem, 22
   4.671 -  \item {\tt mono} constant, 3
   4.672 -  \item {\tt mp} theorem, 5
   4.673 -  \item {\tt mp_tac}, \bold{78}
   4.674 -  \item {\tt mult_assoc} theorem, 80
   4.675 -  \item {\tt mult_commute} theorem, 80
   4.676 -  \item {\tt mult_def} theorem, 80
   4.677 -  \item {\tt mult_typing} theorem, 80
   4.678 -  \item {\tt multC0} theorem, 80
   4.679 -  \item {\tt multC_succ} theorem, 80
   4.680 -  \item {\tt mutual_induct_tac}, \bold{36}
   4.681 +  \item {\tt map} constant, 28
   4.682 +  \item {\tt max} constant, 7, 26
   4.683 +  \item {\tt mem} symbol, 28
   4.684 +  \item {\tt mem_Collect_eq} theorem, 16, 17
   4.685 +  \item {\tt min} constant, 7, 26
   4.686 +  \item {\tt minus} class, 7
   4.687 +  \item {\tt mod} symbol, 25, 83
   4.688 +  \item {\tt mod_def} theorem, 83
   4.689 +  \item {\tt mod_geq} theorem, 26
   4.690 +  \item {\tt mod_less} theorem, 26
   4.691 +  \item {\tt Modal} theory, 1
   4.692 +  \item {\tt mono} constant, 7
   4.693 +  \item {\tt mp} theorem, 9
   4.694 +  \item {\tt mp_tac}, \bold{81}
   4.695 +  \item {\tt mult_assoc} theorem, 83
   4.696 +  \item {\tt mult_commute} theorem, 83
   4.697 +  \item {\tt mult_def} theorem, 83
   4.698 +  \item {\tt mult_typing} theorem, 83
   4.699 +  \item {\tt multC0} theorem, 83
   4.700 +  \item {\tt multC_succ} theorem, 83
   4.701 +  \item {\tt mutual_induct_tac}, \bold{40}
   4.702  
   4.703    \indexspace
   4.704  
   4.705 -  \item {\tt N} constant, 69
   4.706 -  \item {\tt n_not_Suc_n} theorem, 21
   4.707 -  \item {\tt Nat} theory, 22
   4.708 -  \item {\textit {nat}} type, 21, 22
   4.709 -  \item {\textit{nat}} type, 20--23
   4.710 -  \item {\tt nat_induct} theorem, 21
   4.711 -  \item {\tt nat_rec} constant, 22
   4.712 -  \item {\tt NatDef} theory, 20
   4.713 -  \item {\tt NC0} theorem, 73
   4.714 -  \item {\tt NC_succ} theorem, 73
   4.715 -  \item {\tt NE} theorem, 72, 73, 81
   4.716 -  \item {\tt NEL} theorem, 73
   4.717 -  \item {\tt NF} theorem, 73, 82
   4.718 -  \item {\tt NI0} theorem, 73
   4.719 -  \item {\tt NI_succ} theorem, 73
   4.720 -  \item {\tt NI_succL} theorem, 73
   4.721 -  \item {\tt NIO} theorem, 81
   4.722 -  \item {\tt Not} constant, 2, 56
   4.723 -  \item {\tt not_def} theorem, 6
   4.724 -  \item {\tt not_sym} theorem, 7
   4.725 -  \item {\tt notE} theorem, 7
   4.726 -  \item {\tt notI} theorem, 7
   4.727 -  \item {\tt notL} theorem, 58
   4.728 -  \item {\tt notnotD} theorem, 8
   4.729 -  \item {\tt notR} theorem, 58
   4.730 -  \item {\tt null} constant, 24
   4.731 +  \item {\tt N} constant, 72
   4.732 +  \item {\tt n_not_Suc_n} theorem, 25
   4.733 +  \item {\tt Nat} theory, 26
   4.734 +  \item {\textit {nat}} type, 25, 26
   4.735 +  \item {\textit{nat}} type, 24--27
   4.736 +  \item {\tt nat_induct} theorem, 25
   4.737 +  \item {\tt nat_rec} constant, 26
   4.738 +  \item {\tt NatDef} theory, 24
   4.739 +  \item {\tt NC0} theorem, 76
   4.740 +  \item {\tt NC_succ} theorem, 76
   4.741 +  \item {\tt NE} theorem, 75, 76, 84
   4.742 +  \item {\tt NEL} theorem, 76
   4.743 +  \item {\tt NF} theorem, 76, 85
   4.744 +  \item {\tt NI0} theorem, 76
   4.745 +  \item {\tt NI_succ} theorem, 76
   4.746 +  \item {\tt NI_succL} theorem, 76
   4.747 +  \item {\tt NIO} theorem, 84
   4.748 +  \item {\tt Not} constant, 6, 59
   4.749 +  \item {\tt not_def} theorem, 10
   4.750 +  \item {\tt not_sym} theorem, 11
   4.751 +  \item {\tt notE} theorem, 11
   4.752 +  \item {\tt notI} theorem, 11
   4.753 +  \item {\tt notL} theorem, 61
   4.754 +  \item {\tt notnotD} theorem, 12
   4.755 +  \item {\tt notR} theorem, 61
   4.756 +  \item {\tt null} constant, 28
   4.757  
   4.758    \indexspace
   4.759  
   4.760 -  \item {\textit {o}} type, 55
   4.761 -  \item {\tt o} symbol, 2, 13
   4.762 -  \item {\tt o_def} theorem, 6
   4.763 -  \item {\tt of} symbol, 5
   4.764 -  \item {\tt or_def} theorem, 6
   4.765 -  \item {\tt Ord} theory, 3
   4.766 -  \item {\tt ord} class, 3, 4, 22
   4.767 -  \item {\tt order} class, 3, 22
   4.768 +  \item {\textit {o}} type, 58
   4.769 +  \item {\tt o} symbol, 6, 17
   4.770 +  \item {\tt o_def} theorem, 10
   4.771 +  \item {\tt of} symbol, 9
   4.772 +  \item {\tt or_def} theorem, 10
   4.773 +  \item {\tt Ord} theory, 7
   4.774 +  \item {\tt ord} class, 7, 8, 26
   4.775 +  \item {\tt order} class, 7, 26
   4.776  
   4.777    \indexspace
   4.778  
   4.779 -  \item {\tt pack} ML type, 61
   4.780 -  \item {\tt Pair} constant, 19
   4.781 -  \item {\tt pair} constant, 69
   4.782 -  \item {\tt Pair_eq} theorem, 19
   4.783 -  \item {\tt Pair_inject} theorem, 19
   4.784 -  \item {\tt PairE} theorem, 19
   4.785 -  \item {\tt pc_tac}, \bold{63}, \bold{79}, 85, 86
   4.786 -  \item {\tt plus} class, 3
   4.787 -  \item {\tt PlusC_inl} theorem, 75
   4.788 -  \item {\tt PlusC_inr} theorem, 75
   4.789 -  \item {\tt PlusE} theorem, 75, 79, 83
   4.790 -  \item {\tt PlusEL} theorem, 75
   4.791 -  \item {\tt PlusF} theorem, 75
   4.792 -  \item {\tt PlusFL} theorem, 75
   4.793 -  \item {\tt PlusI_inl} theorem, 75, 84
   4.794 -  \item {\tt PlusI_inlL} theorem, 75
   4.795 -  \item {\tt PlusI_inr} theorem, 75
   4.796 -  \item {\tt PlusI_inrL} theorem, 75
   4.797 -  \item {\tt Pow} constant, 10
   4.798 -  \item {\tt Pow_def} theorem, 13
   4.799 -  \item {\tt PowD} theorem, 15
   4.800 -  \item {\tt PowI} theorem, 15
   4.801 -  \item {\tt primrec}, 41--44
   4.802 -  \item {\tt primrec} symbol, 22
   4.803 -  \item {\tt PROD} symbol, 70, 71
   4.804 -  \item {\tt Prod} constant, 69
   4.805 -  \item {\tt Prod} theory, 19
   4.806 -  \item {\tt ProdC} theorem, 73, 89
   4.807 -  \item {\tt ProdC2} theorem, 73
   4.808 -  \item {\tt ProdE} theorem, 73, 86, 88, 90
   4.809 -  \item {\tt ProdEL} theorem, 73
   4.810 -  \item {\tt ProdF} theorem, 73
   4.811 -  \item {\tt ProdFL} theorem, 73
   4.812 -  \item {\tt ProdI} theorem, 73, 79, 81
   4.813 -  \item {\tt ProdIL} theorem, 73
   4.814 -  \item {\tt prop_cs}, \bold{18}
   4.815 -  \item {\tt prop_pack}, \bold{62}
   4.816 +  \item {\tt pack} ML type, 64
   4.817 +  \item {\tt Pair} constant, 23
   4.818 +  \item {\tt pair} constant, 72
   4.819 +  \item {\tt Pair_eq} theorem, 23
   4.820 +  \item {\tt Pair_inject} theorem, 23
   4.821 +  \item {\tt PairE} theorem, 23
   4.822 +  \item {\tt pc_tac}, \bold{66}, \bold{82}, 88, 89
   4.823 +  \item {\tt plus} class, 7
   4.824 +  \item {\tt PlusC_inl} theorem, 78
   4.825 +  \item {\tt PlusC_inr} theorem, 78
   4.826 +  \item {\tt PlusE} theorem, 78, 82, 86
   4.827 +  \item {\tt PlusEL} theorem, 78
   4.828 +  \item {\tt PlusF} theorem, 78
   4.829 +  \item {\tt PlusFL} theorem, 78
   4.830 +  \item {\tt PlusI_inl} theorem, 78, 87
   4.831 +  \item {\tt PlusI_inlL} theorem, 78
   4.832 +  \item {\tt PlusI_inr} theorem, 78
   4.833 +  \item {\tt PlusI_inrL} theorem, 78
   4.834 +  \item {\tt Pow} constant, 14
   4.835 +  \item {\tt Pow_def} theorem, 17
   4.836 +  \item {\tt PowD} theorem, 19
   4.837 +  \item {\tt PowI} theorem, 19
   4.838 +  \item {\tt primrec}, 45--48
   4.839 +  \item {\tt primrec} symbol, 26
   4.840 +  \item priorities, 3
   4.841 +  \item {\tt PROD} symbol, 73, 74
   4.842 +  \item {\tt Prod} constant, 72
   4.843 +  \item {\tt Prod} theory, 23
   4.844 +  \item {\tt ProdC} theorem, 76, 92
   4.845 +  \item {\tt ProdC2} theorem, 76
   4.846 +  \item {\tt ProdE} theorem, 76, 89, 91, 93
   4.847 +  \item {\tt ProdEL} theorem, 76
   4.848 +  \item {\tt ProdF} theorem, 76
   4.849 +  \item {\tt ProdFL} theorem, 76
   4.850 +  \item {\tt ProdI} theorem, 76, 82, 84
   4.851 +  \item {\tt ProdIL} theorem, 76
   4.852 +  \item {\tt prop_cs}, \bold{22}
   4.853 +  \item {\tt prop_pack}, \bold{65}
   4.854  
   4.855    \indexspace
   4.856  
   4.857 -  \item {\tt qed_spec_mp}, 39
   4.858 +  \item {\tt qed_spec_mp}, 43
   4.859  
   4.860    \indexspace
   4.861  
   4.862 -  \item {\tt range} constant, 10, 52
   4.863 -  \item {\tt range_def} theorem, 13
   4.864 -  \item {\tt rangeE} theorem, 15, 53
   4.865 -  \item {\tt rangeI} theorem, 15
   4.866 -  \item {\tt rec} constant, 69, 72
   4.867 -  \item {\tt recdef}, 44--47
   4.868 -  \item {\tt record}, 29
   4.869 -  \item {\tt record_split_tac}, 31, 32
   4.870 +  \item {\tt range} constant, 14, 56
   4.871 +  \item {\tt range_def} theorem, 17
   4.872 +  \item {\tt rangeE} theorem, 19, 56
   4.873 +  \item {\tt rangeI} theorem, 19
   4.874 +  \item {\tt rec} constant, 72, 75
   4.875 +  \item {\tt recdef}, 48--51
   4.876 +  \item {\tt record}, 33
   4.877 +  \item {\tt record_split_tac}, 35, 36
   4.878    \item recursion
   4.879 -    \subitem general, 44--47
   4.880 -    \subitem primitive, 41--44
   4.881 -  \item recursive functions, \see{recursion}{40}
   4.882 -  \item {\tt red_if_equal} theorem, 72
   4.883 -  \item {\tt Reduce} constant, 69, 72, 78
   4.884 -  \item {\tt refl} theorem, 5, 58
   4.885 -  \item {\tt refl_elem} theorem, 72, 76
   4.886 -  \item {\tt refl_red} theorem, 72
   4.887 -  \item {\tt refl_type} theorem, 72, 76
   4.888 -  \item {\tt REPEAT_FIRST}, 77
   4.889 -  \item {\tt repeat_goal_tac}, \bold{63}
   4.890 -  \item {\tt replace_type} theorem, 76, 88
   4.891 -  \item {\tt reresolve_tac}, \bold{63}
   4.892 -  \item {\tt res_inst_tac}, 4
   4.893 -  \item {\tt rev} constant, 24
   4.894 -  \item {\tt rew_tac}, \bold{78}
   4.895 -  \item {\tt RL}, 83
   4.896 -  \item {\tt RS}, 88, 90
   4.897 +    \subitem general, 48--51
   4.898 +    \subitem primitive, 45--48
   4.899 +  \item recursive functions, \see{recursion}{44}
   4.900 +  \item {\tt red_if_equal} theorem, 75
   4.901 +  \item {\tt Reduce} constant, 72, 75, 81
   4.902 +  \item {\tt refl} theorem, 9, 61
   4.903 +  \item {\tt refl_elem} theorem, 75, 79
   4.904 +  \item {\tt refl_red} theorem, 75
   4.905 +  \item {\tt refl_type} theorem, 75, 79
   4.906 +  \item {\tt REPEAT_FIRST}, 80
   4.907 +  \item {\tt repeat_goal_tac}, \bold{66}
   4.908 +  \item {\tt replace_type} theorem, 79, 91
   4.909 +  \item {\tt reresolve_tac}, \bold{66}
   4.910 +  \item {\tt res_inst_tac}, 8
   4.911 +  \item {\tt rev} constant, 28
   4.912 +  \item {\tt rew_tac}, \bold{81}
   4.913 +  \item {\tt RL}, 86
   4.914 +  \item {\tt RS}, 91, 93
   4.915  
   4.916    \indexspace
   4.917  
   4.918 -  \item {\tt safe_goal_tac}, \bold{63}
   4.919 -  \item {\tt safe_tac}, \bold{79}
   4.920 -  \item {\tt safestep_tac}, \bold{79}
   4.921 +  \item {\tt safe_goal_tac}, \bold{66}
   4.922 +  \item {\tt safe_tac}, \bold{82}
   4.923 +  \item {\tt safestep_tac}, \bold{82}
   4.924    \item search
   4.925 -    \subitem best-first, 54
   4.926 -  \item {\tt select_equality} theorem, 6, 8
   4.927 -  \item {\tt selectI} theorem, 5, 6
   4.928 -  \item {\tt Seqof} constant, 56
   4.929 -  \item sequent calculus, 55--67
   4.930 -  \item {\tt Set} theory, 9, 12
   4.931 -  \item {\tt set} constant, 24
   4.932 -  \item {\tt set} type, 9
   4.933 -  \item {\tt set_current_thy}, 54
   4.934 -  \item {\tt set_diff_def} theorem, 13
   4.935 -  \item {\tt show_sorts}, 4
   4.936 -  \item {\tt show_types}, 4
   4.937 -  \item {\tt Sigma} constant, 19
   4.938 -  \item {\tt Sigma_def} theorem, 19
   4.939 -  \item {\tt SigmaE} theorem, 19
   4.940 -  \item {\tt SigmaI} theorem, 19
   4.941 +    \subitem best-first, 57
   4.942 +  \item {\tt select_equality} theorem, 10, 12
   4.943 +  \item {\tt selectI} theorem, 9, 10
   4.944 +  \item {\tt Seqof} constant, 59
   4.945 +  \item sequent calculus, 58--70
   4.946 +  \item {\tt Set} theory, 13, 16
   4.947 +  \item {\tt set} constant, 28
   4.948 +  \item {\tt set} type, 13
   4.949 +  \item {\tt set_current_thy}, 57
   4.950 +  \item {\tt set_diff_def} theorem, 17
   4.951 +  \item {\tt show_sorts}, 8
   4.952 +  \item {\tt show_types}, 8
   4.953 +  \item {\tt Sigma} constant, 23
   4.954 +  \item {\tt Sigma_def} theorem, 23
   4.955 +  \item {\tt SigmaE} theorem, 23
   4.956 +  \item {\tt SigmaI} theorem, 23
   4.957    \item simplification
   4.958 -    \subitem of conjunctions, 17
   4.959 -  \item {\tt size} constant, 35
   4.960 -  \item {\tt snd} constant, 19, 69, 74
   4.961 -  \item {\tt snd_conv} theorem, 19
   4.962 -  \item {\tt snd_def} theorem, 74
   4.963 -  \item {\tt sobj} type, 59
   4.964 -  \item {\tt spec} theorem, 8
   4.965 -  \item {\tt split} constant, 19, 69, 83
   4.966 -  \item {\tt split} theorem, 19
   4.967 -  \item {\tt split_all_tac}, \bold{20}
   4.968 -  \item {\tt split_if} theorem, 8, 18
   4.969 -  \item {\tt split_list_case} theorem, 23
   4.970 -  \item {\tt split_split} theorem, 19
   4.971 -  \item {\tt split_sum_case} theorem, 21
   4.972 -  \item {\tt ssubst} theorem, 7, 9
   4.973 -  \item {\tt stac}, \bold{17}
   4.974 -  \item {\tt step_tac}, \bold{63}, \bold{79}
   4.975 -  \item {\tt strip_tac}, \bold{9}
   4.976 -  \item {\tt subset_def} theorem, 13
   4.977 -  \item {\tt subset_refl} theorem, 14
   4.978 -  \item {\tt subset_trans} theorem, 14
   4.979 -  \item {\tt subsetCE} theorem, 12, 14
   4.980 -  \item {\tt subsetD} theorem, 12, 14
   4.981 -  \item {\tt subsetI} theorem, 14
   4.982 -  \item {\tt subst} theorem, 5
   4.983 -  \item {\tt subst_elem} theorem, 72
   4.984 -  \item {\tt subst_elemL} theorem, 72
   4.985 -  \item {\tt subst_eqtyparg} theorem, 76, 88
   4.986 -  \item {\tt subst_prodE} theorem, 74, 76
   4.987 -  \item {\tt subst_type} theorem, 72
   4.988 -  \item {\tt subst_typeL} theorem, 72
   4.989 -  \item {\tt Suc} constant, 21
   4.990 -  \item {\tt Suc_not_Zero} theorem, 21
   4.991 -  \item {\tt succ} constant, 69
   4.992 -  \item {\tt SUM} symbol, 70, 71
   4.993 -  \item {\tt Sum} constant, 69
   4.994 -  \item {\tt Sum} theory, 20
   4.995 -  \item {\tt sum_case} constant, 21
   4.996 -  \item {\tt sum_case_Inl} theorem, 21
   4.997 -  \item {\tt sum_case_Inr} theorem, 21
   4.998 -  \item {\tt SumC} theorem, 74
   4.999 -  \item {\tt SumE} theorem, 74, 79, 83
  4.1000 -  \item {\tt sumE} theorem, 21
  4.1001 -  \item {\tt SumE_fst} theorem, 74, 76, 88, 89
  4.1002 -  \item {\tt SumE_snd} theorem, 74, 76, 90
  4.1003 -  \item {\tt SumEL} theorem, 74
  4.1004 -  \item {\tt SumF} theorem, 74
  4.1005 -  \item {\tt SumFL} theorem, 74
  4.1006 -  \item {\tt SumI} theorem, 74, 84
  4.1007 -  \item {\tt SumIL} theorem, 74
  4.1008 -  \item {\tt SumIL2} theorem, 76
  4.1009 -  \item {\tt surj} constant, 13, 17
  4.1010 -  \item {\tt surj_def} theorem, 17
  4.1011 -  \item {\tt surjective_pairing} theorem, 19
  4.1012 -  \item {\tt surjective_sum} theorem, 21
  4.1013 -  \item {\tt swap} theorem, 8
  4.1014 -  \item {\tt swap_res_tac}, 53
  4.1015 -  \item {\tt sym} theorem, 7, 58
  4.1016 -  \item {\tt sym_elem} theorem, 72
  4.1017 -  \item {\tt sym_type} theorem, 72
  4.1018 -  \item {\tt symL} theorem, 59
  4.1019 +    \subitem of conjunctions, 21
  4.1020 +  \item {\tt size} constant, 40
  4.1021 +  \item {\tt snd} constant, 23, 72, 77
  4.1022 +  \item {\tt snd_conv} theorem, 23
  4.1023 +  \item {\tt snd_def} theorem, 77
  4.1024 +  \item {\tt sobj} type, 62
  4.1025 +  \item {\tt spec} theorem, 12
  4.1026 +  \item {\tt split} constant, 23, 72, 86
  4.1027 +  \item {\tt split} theorem, 23
  4.1028 +  \item {\tt split_all_tac}, \bold{24}
  4.1029 +  \item {\tt split_if} theorem, 12, 22
  4.1030 +  \item {\tt split_list_case} theorem, 27
  4.1031 +  \item {\tt split_split} theorem, 23
  4.1032 +  \item {\tt split_sum_case} theorem, 25
  4.1033 +  \item {\tt ssubst} theorem, 11, 13
  4.1034 +  \item {\tt stac}, \bold{21}
  4.1035 +  \item {\tt step_tac}, \bold{66}, \bold{82}
  4.1036 +  \item {\tt strip_tac}, \bold{13}
  4.1037 +  \item {\tt subset_def} theorem, 17
  4.1038 +  \item {\tt subset_refl} theorem, 18
  4.1039 +  \item {\tt subset_trans} theorem, 18
  4.1040 +  \item {\tt subsetCE} theorem, 16, 18
  4.1041 +  \item {\tt subsetD} theorem, 16, 18
  4.1042 +  \item {\tt subsetI} theorem, 18
  4.1043 +  \item {\tt subst} theorem, 9
  4.1044 +  \item {\tt subst_elem} theorem, 75
  4.1045 +  \item {\tt subst_elemL} theorem, 75
  4.1046 +  \item {\tt subst_eqtyparg} theorem, 79, 91
  4.1047 +  \item {\tt subst_prodE} theorem, 77, 79
  4.1048 +  \item {\tt subst_type} theorem, 75
  4.1049 +  \item {\tt subst_typeL} theorem, 75
  4.1050 +  \item {\tt Suc} constant, 25
  4.1051 +  \item {\tt Suc_not_Zero} theorem, 25
  4.1052 +  \item {\tt succ} constant, 72
  4.1053 +  \item {\tt SUM} symbol, 73, 74
  4.1054 +  \item {\tt Sum} constant, 72
  4.1055 +  \item {\tt Sum} theory, 24
  4.1056 +  \item {\tt sum_case} constant, 25
  4.1057 +  \item {\tt sum_case_Inl} theorem, 25
  4.1058 +  \item {\tt sum_case_Inr} theorem, 25
  4.1059 +  \item {\tt SumC} theorem, 77
  4.1060 +  \item {\tt SumE} theorem, 77, 82, 86
  4.1061 +  \item {\tt sumE} theorem, 25
  4.1062 +  \item {\tt SumE_fst} theorem, 77, 79, 91, 92
  4.1063 +  \item {\tt SumE_snd} theorem, 77, 79, 93
  4.1064 +  \item {\tt SumEL} theorem, 77
  4.1065 +  \item {\tt SumF} theorem, 77
  4.1066 +  \item {\tt SumFL} theorem, 77
  4.1067 +  \item {\tt SumI} theorem, 77, 87
  4.1068 +  \item {\tt SumIL} theorem, 77
  4.1069 +  \item {\tt SumIL2} theorem, 79
  4.1070 +  \item {\tt surj} constant, 17, 21
  4.1071 +  \item {\tt surj_def} theorem, 21
  4.1072 +  \item {\tt surjective_pairing} theorem, 23
  4.1073 +  \item {\tt surjective_sum} theorem, 25
  4.1074 +  \item {\tt swap} theorem, 12
  4.1075 +  \item {\tt swap_res_tac}, 57
  4.1076 +  \item {\tt sym} theorem, 11, 61
  4.1077 +  \item {\tt sym_elem} theorem, 75
  4.1078 +  \item {\tt sym_type} theorem, 75
  4.1079 +  \item {\tt symL} theorem, 62
  4.1080  
  4.1081    \indexspace
  4.1082  
  4.1083 -  \item {\tt T} constant, 69
  4.1084 -  \item {\textit {t}} type, 68
  4.1085 -  \item {\tt take} constant, 24
  4.1086 -  \item {\tt takeWhile} constant, 24
  4.1087 -  \item {\tt TC} theorem, 75
  4.1088 -  \item {\tt TE} theorem, 75
  4.1089 -  \item {\tt TEL} theorem, 75
  4.1090 -  \item {\tt term} class, 3, 55
  4.1091 -  \item {\tt test_assume_tac}, \bold{77}
  4.1092 -  \item {\tt TF} theorem, 75
  4.1093 -  \item {\tt THE} symbol, 56
  4.1094 -  \item {\tt The} constant, 56
  4.1095 -  \item {\tt The} theorem, 58
  4.1096 -  \item {\tt thinL} theorem, 58
  4.1097 -  \item {\tt thinR} theorem, 58
  4.1098 -  \item {\tt TI} theorem, 75
  4.1099 -  \item {\tt times} class, 3
  4.1100 -  \item {\tt tl} constant, 24
  4.1101 +  \item {\tt T} constant, 72
  4.1102 +  \item {\textit {t}} type, 71
  4.1103 +  \item {\tt take} constant, 28
  4.1104 +  \item {\tt takeWhile} constant, 28
  4.1105 +  \item {\tt TC} theorem, 78
  4.1106 +  \item {\tt TE} theorem, 78
  4.1107 +  \item {\tt TEL} theorem, 78
  4.1108 +  \item {\tt term} class, 7, 58
  4.1109 +  \item {\tt test_assume_tac}, \bold{80}
  4.1110 +  \item {\tt TF} theorem, 78
  4.1111 +  \item {\tt THE} symbol, 59
  4.1112 +  \item {\tt The} constant, 59
  4.1113 +  \item {\tt The} theorem, 61
  4.1114 +  \item {\tt thinL} theorem, 61
  4.1115 +  \item {\tt thinR} theorem, 61
  4.1116 +  \item {\tt TI} theorem, 78
  4.1117 +  \item {\tt times} class, 7
  4.1118 +  \item {\tt tl} constant, 28
  4.1119    \item tracing
  4.1120 -    \subitem of unification, 4
  4.1121 -  \item {\tt trans} theorem, 7, 58
  4.1122 -  \item {\tt trans_elem} theorem, 72
  4.1123 -  \item {\tt trans_red} theorem, 72
  4.1124 -  \item {\tt trans_tac}, 23
  4.1125 -  \item {\tt trans_type} theorem, 72
  4.1126 -  \item {\tt True} constant, 2, 56
  4.1127 -  \item {\tt True_def} theorem, 6, 58
  4.1128 -  \item {\tt True_or_False} theorem, 5, 6
  4.1129 -  \item {\tt TrueI} theorem, 7
  4.1130 -  \item {\tt Trueprop} constant, 2, 56
  4.1131 -  \item {\tt TrueR} theorem, 59
  4.1132 -  \item {\tt tt} constant, 69
  4.1133 -  \item {\tt Type} constant, 69
  4.1134 -  \item type definition, \bold{26}
  4.1135 -  \item {\tt typechk_tac}, \bold{77}, 82, 85, 89, 90
  4.1136 -  \item {\tt typedef}, 23
  4.1137 +    \subitem of unification, 8
  4.1138 +  \item {\tt trans} theorem, 11, 61
  4.1139 +  \item {\tt trans_elem} theorem, 75
  4.1140 +  \item {\tt trans_red} theorem, 75
  4.1141 +  \item {\tt trans_tac}, 27
  4.1142 +  \item {\tt trans_type} theorem, 75
  4.1143 +  \item {\tt True} constant, 6, 59
  4.1144 +  \item {\tt True_def} theorem, 10, 61
  4.1145 +  \item {\tt True_or_False} theorem, 9, 10
  4.1146 +  \item {\tt TrueI} theorem, 11
  4.1147 +  \item {\tt Trueprop} constant, 6, 59
  4.1148 +  \item {\tt TrueR} theorem, 62
  4.1149 +  \item {\tt tt} constant, 72
  4.1150 +  \item {\tt Type} constant, 72
  4.1151 +  \item type definition, \bold{30}
  4.1152 +  \item {\tt typechk_tac}, \bold{80}, 85, 88, 92, 93
  4.1153 +  \item {\tt typedef}, 27
  4.1154  
  4.1155    \indexspace
  4.1156  
  4.1157 -  \item {\tt UN} symbol, 10--12
  4.1158 -  \item {\tt Un} symbol, 10
  4.1159 -  \item {\tt Un1} theorem, 12
  4.1160 -  \item {\tt Un2} theorem, 12
  4.1161 -  \item {\tt Un_absorb} theorem, 16
  4.1162 -  \item {\tt Un_assoc} theorem, 16
  4.1163 -  \item {\tt Un_commute} theorem, 16
  4.1164 -  \item {\tt Un_def} theorem, 13
  4.1165 -  \item {\tt UN_E} theorem, 15
  4.1166 -  \item {\tt UN_I} theorem, 15
  4.1167 -  \item {\tt Un_Int_distrib} theorem, 16
  4.1168 -  \item {\tt Un_Inter} theorem, 16
  4.1169 -  \item {\tt Un_least} theorem, 16
  4.1170 -  \item {\tt Un_Union_image} theorem, 16
  4.1171 -  \item {\tt Un_upper1} theorem, 16
  4.1172 -  \item {\tt Un_upper2} theorem, 16
  4.1173 -  \item {\tt UnCI} theorem, 12, 15
  4.1174 -  \item {\tt UnE} theorem, 15
  4.1175 -  \item {\tt UnI1} theorem, 15
  4.1176 -  \item {\tt UnI2} theorem, 15
  4.1177 +  \item {\tt UN} symbol, 14--16
  4.1178 +  \item {\tt Un} symbol, 14
  4.1179 +  \item {\tt Un1} theorem, 16
  4.1180 +  \item {\tt Un2} theorem, 16
  4.1181 +  \item {\tt Un_absorb} theorem, 20
  4.1182 +  \item {\tt Un_assoc} theorem, 20
  4.1183 +  \item {\tt Un_commute} theorem, 20
  4.1184 +  \item {\tt Un_def} theorem, 17
  4.1185 +  \item {\tt UN_E} theorem, 19
  4.1186 +  \item {\tt UN_I} theorem, 19
  4.1187 +  \item {\tt Un_Int_distrib} theorem, 20
  4.1188 +  \item {\tt Un_Inter} theorem, 20
  4.1189 +  \item {\tt Un_least} theorem, 20
  4.1190 +  \item {\tt Un_Union_image} theorem, 20
  4.1191 +  \item {\tt Un_upper1} theorem, 20
  4.1192 +  \item {\tt Un_upper2} theorem, 20
  4.1193 +  \item {\tt UnCI} theorem, 16, 19
  4.1194 +  \item {\tt UnE} theorem, 19
  4.1195 +  \item {\tt UnI1} theorem, 19
  4.1196 +  \item {\tt UnI2} theorem, 19
  4.1197    \item unification
  4.1198 -    \subitem incompleteness of, 4
  4.1199 -  \item {\tt Unify.trace_types}, 4
  4.1200 -  \item {\tt UNION} constant, 10
  4.1201 -  \item {\tt Union} constant, 10
  4.1202 -  \item {\tt UNION1} constant, 10
  4.1203 -  \item {\tt UNION1_def} theorem, 13
  4.1204 -  \item {\tt UNION_def} theorem, 13
  4.1205 -  \item {\tt Union_def} theorem, 13
  4.1206 -  \item {\tt Union_least} theorem, 16
  4.1207 -  \item {\tt Union_Un_distrib} theorem, 16
  4.1208 -  \item {\tt Union_upper} theorem, 16
  4.1209 -  \item {\tt UnionE} theorem, 15
  4.1210 -  \item {\tt UnionI} theorem, 15
  4.1211 -  \item {\tt unit_eq} theorem, 20
  4.1212 +    \subitem incompleteness of, 8
  4.1213 +  \item {\tt Unify.trace_types}, 8
  4.1214 +  \item {\tt UNION} constant, 14
  4.1215 +  \item {\tt Union} constant, 14
  4.1216 +  \item {\tt UNION1} constant, 14
  4.1217 +  \item {\tt UNION1_def} theorem, 17
  4.1218 +  \item {\tt UNION_def} theorem, 17
  4.1219 +  \item {\tt Union_def} theorem, 17
  4.1220 +  \item {\tt Union_least} theorem, 20
  4.1221 +  \item {\tt Union_Un_distrib} theorem, 20
  4.1222 +  \item {\tt Union_upper} theorem, 20
  4.1223 +  \item {\tt UnionE} theorem, 19
  4.1224 +  \item {\tt UnionI} theorem, 19
  4.1225 +  \item {\tt unit_eq} theorem, 24
  4.1226  
  4.1227    \indexspace
  4.1228  
  4.1229 -  \item {\tt when} constant, 69, 74, 83
  4.1230 +  \item {\tt when} constant, 72, 77, 86
  4.1231  
  4.1232    \indexspace
  4.1233  
  4.1234 -  \item {\tt zero_ne_succ} theorem, 72, 73
  4.1235 -  \item {\tt ZF} theory, 1
  4.1236 +  \item {\tt zero_ne_succ} theorem, 75, 76
  4.1237 +  \item {\tt ZF} theory, 5
  4.1238  
  4.1239  \end{theindex}
     5.1 --- a/doc-src/ZF/ZF.tex	Tue Jan 19 11:16:39 1999 +0100
     5.2 +++ b/doc-src/ZF/ZF.tex	Tue Jan 19 11:18:11 1999 +0100
     5.3 @@ -1669,7 +1669,7 @@
     5.4  val free_iffs     : thm list  \textrm{logical equivalences for proving freeness}
     5.5  val free_SEs      : thm list  \textrm{elimination rules for proving freeness}
     5.6  val mk_free       : string -> thm  \textrm{A function for proving freeness theorems}
     5.7 -val mk_cases      : thm list -> string -> thm  \textrm{case analysis, see below}
     5.8 +val mk_cases      : string -> thm  \textrm{case analysis, see below}
     5.9  val defs          : thm list  \textrm{definitions of operators}
    5.10  val bnd_mono      : thm list  \textrm{monotonicity property}
    5.11  val dom_subset    : thm list  \textrm{inclusion in `bounding set'}
    5.12 @@ -1746,13 +1746,12 @@
    5.13  {\out                     ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm}
    5.14  \end{ttbox}
    5.15  
    5.16 -The purpose of \ttindex{mk_cases} is to generate simplified instances of the
    5.17 -elimination (case analysis) rule.  Its theorem list argument is a list of
    5.18 -constructor definitions, which it uses for freeness reasoning.  For example,
    5.19 -this instance of the elimination rule propagates type-checking information
    5.20 -from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$:
    5.21 +The purpose of \ttindex{mk_cases} is to generate instances of the elimination
    5.22 +(case analysis) rule that have been simplified using freeness reasoning.  For
    5.23 +example, this instance of the elimination rule propagates type-checking
    5.24 +information from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$:
    5.25  \begin{ttbox}
    5.26 -val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)";
    5.27 +val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
    5.28  {\out val BrE =}
    5.29  {\out   "[| Br(?a, ?l, ?r) : bt(?A);}
    5.30  {\out       [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm}
    5.31 @@ -2130,7 +2129,7 @@
    5.32  \begin{ttbox}
    5.33  val intrs         : thm list  \textrm{the introduction rules}
    5.34  val elim          : thm       \textrm{the elimination (case analysis) rule}
    5.35 -val mk_cases      : thm list -> string -> thm  \textrm{case analysis, see below}
    5.36 +val mk_cases      : string -> thm  \textrm{case analysis, see below}
    5.37  val induct        : thm       \textrm{the standard induction rule}
    5.38  val mutual_induct : thm       \textrm{the mutual induction rule, or \texttt{True}}
    5.39  val defs          : thm list  \textrm{definitions of operators}
    5.40 @@ -2160,7 +2159,7 @@
    5.41  inductively.  Then the file \texttt{ex/Comb.ML} defines special cases of
    5.42  contraction using \texttt{mk_cases}:
    5.43  \begin{ttbox}
    5.44 -val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
    5.45 +val K_contractE = contract.mk_cases "K -1-> r";
    5.46  {\out val K_contractE = "K -1-> ?r ==> ?Q" : thm}
    5.47  \end{ttbox}
    5.48  We can read this as saying that the combinator \texttt{K} cannot reduce to
     6.1 --- a/src/HOL/Auth/Message.ML	Tue Jan 19 11:16:39 1999 +0100
     6.2 +++ b/src/HOL/Auth/Message.ML	Tue Jan 19 11:18:11 1999 +0100
     6.3 @@ -576,16 +576,12 @@
     6.4  
     6.5  AddIs  synth.intrs;
     6.6  
     6.7 -(*Can only produce a nonce or key if it is already known,
     6.8 -  but can synth a pair or encryption from its components...*)
     6.9 -val mk_cases = synth.mk_cases (atomic.simps @ msg.simps);
    6.10 -
    6.11  (*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
    6.12 -val Nonce_synth = mk_cases "Nonce n : synth H";
    6.13 -val Key_synth   = mk_cases "Key K : synth H";
    6.14 -val Hash_synth  = mk_cases "Hash X : synth H";
    6.15 -val MPair_synth = mk_cases "{|X,Y|} : synth H";
    6.16 -val Crypt_synth = mk_cases "Crypt K X : synth H";
    6.17 +val Nonce_synth = synth.mk_cases "Nonce n : synth H";
    6.18 +val Key_synth   = synth.mk_cases "Key K : synth H";
    6.19 +val Hash_synth  = synth.mk_cases "Hash X : synth H";
    6.20 +val MPair_synth = synth.mk_cases "{|X,Y|} : synth H";
    6.21 +val Crypt_synth = synth.mk_cases "Crypt K X : synth H";
    6.22  
    6.23  AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
    6.24  
     7.1 --- a/src/HOL/Finite.ML	Tue Jan 19 11:16:39 1999 +0100
     7.2 +++ b/src/HOL/Finite.ML	Tue Jan 19 11:18:11 1999 +0100
     7.3 @@ -325,9 +325,9 @@
     7.4  Addsimps [card_insert_disjoint];
     7.5  *)
     7.6  
     7.7 -val cardR_emptyE = cardR.mk_cases [] "({},n) : cardR";
     7.8 +val cardR_emptyE = cardR.mk_cases "({},n) : cardR";
     7.9  AddSEs [cardR_emptyE];
    7.10 -val cardR_insertE = cardR.mk_cases [] "(insert a A,n) : cardR";
    7.11 +val cardR_insertE = cardR.mk_cases "(insert a A,n) : cardR";
    7.12  AddSIs cardR.intrs;
    7.13  
    7.14  Goal "[| (A,n) : cardR |] ==> a : A --> (? m. n = Suc m)";
    7.15 @@ -565,7 +565,7 @@
    7.16  
    7.17  (*** foldSet ***)
    7.18  
    7.19 -val empty_foldSetE = foldSet.mk_cases [] "({}, x) : foldSet f e";
    7.20 +val empty_foldSetE = foldSet.mk_cases "({}, x) : foldSet f e";
    7.21  
    7.22  AddSEs [empty_foldSetE];
    7.23  AddIs foldSet.intrs;
     8.1 --- a/src/HOL/IMP/Expr.ML	Tue Jan 19 11:16:39 1999 +0100
     8.2 +++ b/src/HOL/IMP/Expr.ML	Tue Jan 19 11:18:11 1999 +0100
     8.3 @@ -7,16 +7,21 @@
     8.4  Not used in the rest of the language, but included for completeness.
     8.5  *)
     8.6  
     8.7 -val evala_elim_cases = map (evala.mk_cases aexp.simps)
     8.8 -   ["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i",
     8.9 -    "(Op1 f e,sigma) -a-> i", "(Op2 f a1 a2,sigma)  -a-> i"
    8.10 -   ];
    8.11 +val evala_elim_cases = 
    8.12 +    map evala.mk_cases
    8.13 +       ["(N(n),sigma) -a-> i", 
    8.14 +	"(X(x),sigma) -a-> i",
    8.15 +	"(Op1 f e,sigma) -a-> i", 
    8.16 +	"(Op2 f a1 a2,sigma)  -a-> i"];
    8.17  
    8.18 -val evalb_elim_cases = map (evalb.mk_cases bexp.simps)
    8.19 -   ["(true,sigma) -b-> x", "(false,sigma) -b-> x",
    8.20 -    "(ROp f a0 a1,sigma) -b-> x", "(noti(b),sigma) -b-> x",
    8.21 -    "(b0 andi b1,sigma) -b-> x", "(b0 ori b1,sigma) -b-> x"
    8.22 -   ];
    8.23 +val evalb_elim_cases = 
    8.24 +    map evalb.mk_cases
    8.25 +       ["(true,sigma) -b-> x", 
    8.26 +	"(false,sigma) -b-> x",
    8.27 +	"(ROp f a0 a1,sigma) -b-> x", 
    8.28 +	"(noti(b),sigma) -b-> x",
    8.29 +	"(b0 andi b1,sigma) -b-> x", 
    8.30 +	"(b0 ori b1,sigma) -b-> x"];
    8.31  
    8.32  val evalb_simps = map (fn s => prove_goal Expr.thy s
    8.33      (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
     9.1 --- a/src/HOL/IMP/Natural.ML	Tue Jan 19 11:16:39 1999 +0100
     9.2 +++ b/src/HOL/IMP/Natural.ML	Tue Jan 19 11:18:11 1999 +0100
     9.3 @@ -8,11 +8,14 @@
     9.4  
     9.5  AddIs evalc.intrs;
     9.6  
     9.7 -val evalc_elim_cases = map (evalc.mk_cases com.simps)
     9.8 -   ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
     9.9 -    "<IF b THEN c1 ELSE c2, s> -c-> t"];
    9.10 +val evalc_elim_cases = 
    9.11 +    map evalc.mk_cases
    9.12 +       ["<SKIP,s> -c-> t", 
    9.13 +	"<x:=a,s> -c-> t", 
    9.14 +	"<c1;c2, s> -c-> t",
    9.15 +	"<IF b THEN c1 ELSE c2, s> -c-> t"];
    9.16  
    9.17 -val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
    9.18 +val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
    9.19  
    9.20  AddSEs evalc_elim_cases;
    9.21  
    10.1 --- a/src/HOL/IMP/Transition.ML	Tue Jan 19 11:16:39 1999 +0100
    10.2 +++ b/src/HOL/IMP/Transition.ML	Tue Jan 19 11:18:11 1999 +0100
    10.3 @@ -10,11 +10,14 @@
    10.4  
    10.5  AddSEs [rel_pow_0_E];
    10.6  
    10.7 -val evalc1_SEs = map (evalc1.mk_cases com.simps)
    10.8 -   ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t","(c1;c2, s) -1-> t", 
    10.9 -    "(IF b THEN c1 ELSE c2, s) -1-> t"];
   10.10 -val evalc1_Es = map (evalc1.mk_cases com.simps)
   10.11 -   ["(WHILE b DO c,s) -1-> t"];
   10.12 +val evalc1_SEs = 
   10.13 +    map evalc1.mk_cases
   10.14 +       ["(SKIP,s) -1-> t", 
   10.15 +	"(x:=a,s) -1-> t",
   10.16 +	"(c1;c2, s) -1-> t", 
   10.17 +	"(IF b THEN c1 ELSE c2, s) -1-> t"];
   10.18 +
   10.19 +val evalc1_E = evalc1.mk_cases "(WHILE b DO c,s) -1-> t";
   10.20  
   10.21  AddSEs evalc1_SEs;
   10.22  
   10.23 @@ -95,7 +98,7 @@
   10.24  by (strip_tac 1);
   10.25  by (etac rel_pow_E2 1);
   10.26   by (Asm_full_simp_tac 1);
   10.27 -by (eresolve_tac evalc1_Es 1);
   10.28 +by (etac evalc1_E 1);
   10.29  
   10.30  (* WhileFalse *)
   10.31   by (fast_tac (claset() addSDs [hlemma]) 1);
    11.1 --- a/src/HOL/Induct/Com.ML	Tue Jan 19 11:16:39 1999 +0100
    11.2 +++ b/src/HOL/Induct/Com.ML	Tue Jan 19 11:18:11 1999 +0100
    11.3 @@ -8,11 +8,14 @@
    11.4  
    11.5  AddIs exec.intrs;
    11.6  
    11.7 -val exec_elim_cases = map (exec.mk_cases exp.simps)
    11.8 -   ["(SKIP,s) -[eval]-> t", "(x:=a,s) -[eval]-> t", "(c1;;c2, s) -[eval]-> t",
    11.9 -    "(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
   11.10 +val exec_elim_cases = 
   11.11 +    map exec.mk_cases
   11.12 +       ["(SKIP,s) -[eval]-> t",
   11.13 +	"(x:=a,s) -[eval]-> t", 
   11.14 +	"(c1;;c2, s) -[eval]-> t",
   11.15 +	"(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
   11.16  
   11.17 -val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) -[eval]-> t";
   11.18 +val exec_WHILE_case = exec.mk_cases "(WHILE b DO c,s) -[eval]-> t";
   11.19  
   11.20  AddSEs exec_elim_cases;
   11.21  
    12.1 --- a/src/HOL/Induct/Comb.ML	Tue Jan 19 11:16:39 1999 +0100
    12.2 +++ b/src/HOL/Induct/Comb.ML	Tue Jan 19 11:18:11 1999 +0100
    12.3 @@ -45,9 +45,9 @@
    12.4  (*** Results about Contraction ***)
    12.5  
    12.6  (*Derive a case for each combinator constructor*)
    12.7 -val K_contractE = contract.mk_cases comb.simps "K -1-> z";
    12.8 -val S_contractE = contract.mk_cases comb.simps "S -1-> z";
    12.9 -val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
   12.10 +val K_contractE  = contract.mk_cases "K -1-> z";
   12.11 +val S_contractE  = contract.mk_cases "S -1-> z";
   12.12 +val Ap_contractE = contract.mk_cases "x#y -1-> z";
   12.13  
   12.14  AddSIs [contract.K, contract.S];
   12.15  AddIs  [contract.Ap1, contract.Ap2];
   12.16 @@ -96,9 +96,9 @@
   12.17  (*** Results about Parallel Contraction ***)
   12.18  
   12.19  (*Derive a case for each combinator constructor*)
   12.20 -val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
   12.21 -val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
   12.22 -val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
   12.23 +val K_parcontractE  = parcontract.mk_cases "K =1=> z";
   12.24 +val S_parcontractE  = parcontract.mk_cases "S =1=> z";
   12.25 +val Ap_parcontractE = parcontract.mk_cases "x#y =1=> z";
   12.26  
   12.27  AddSIs [parcontract.refl, parcontract.K, parcontract.S];
   12.28  AddIs  [parcontract.Ap];
    13.1 --- a/src/HOL/Induct/Exp.ML	Tue Jan 19 11:16:39 1999 +0100
    13.2 +++ b/src/HOL/Induct/Exp.ML	Tue Jan 19 11:18:11 1999 +0100
    13.3 @@ -9,11 +9,12 @@
    13.4  AddSIs [eval.N, eval.X];
    13.5  AddIs  [eval.Op, eval.valOf];
    13.6  
    13.7 -val eval_elim_cases = map (eval.mk_cases exp.simps)
    13.8 -   ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
    13.9 -    "(Op f a1 a2,sigma)  -|-> (n,s')",
   13.10 -    "(VALOF c RESULTIS e, s) -|-> (n, s1)"
   13.11 -   ];
   13.12 +val eval_elim_cases = 
   13.13 +    map eval.mk_cases 
   13.14 +       ["(N(n),sigma) -|-> (n',s')", 
   13.15 +	"(X(x),sigma) -|-> (n,s')",
   13.16 +	"(Op f a1 a2,sigma)  -|-> (n,s')",
   13.17 +	"(VALOF c RESULTIS e, s) -|-> (n, s1)"];
   13.18  
   13.19  AddSEs eval_elim_cases;
   13.20  
    14.1 --- a/src/HOL/Induct/LFilter.ML	Tue Jan 19 11:16:39 1999 +0100
    14.2 +++ b/src/HOL/Induct/LFilter.ML	Tue Jan 19 11:18:11 1999 +0100
    14.3 @@ -9,8 +9,7 @@
    14.4  
    14.5  (*** findRel: basic laws ****)
    14.6  
    14.7 -val findRel_LConsE = 
    14.8 -    findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p";
    14.9 +val findRel_LConsE = findRel.mk_cases "(LCons x l, l'') : findRel p";
   14.10  
   14.11  AddSEs [findRel_LConsE];
   14.12  
    15.1 --- a/src/HOL/Lambda/Eta.ML	Tue Jan 19 11:16:39 1999 +0100
    15.2 +++ b/src/HOL/Lambda/Eta.ML	Tue Jan 19 11:18:11 1999 +0100
    15.3 @@ -12,8 +12,7 @@
    15.4  Addsimps eta.intrs;
    15.5  AddIs eta.intrs;
    15.6  
    15.7 -val eta_cases = map (eta.mk_cases dB.simps)
    15.8 -    ["Abs s -e> z","s $ t -e> u","Var i -e> t"];
    15.9 +val eta_cases = map eta.mk_cases ["Abs s -e> z", "s $ t -e> u", "Var i -e> t"];
   15.10  AddSEs eta_cases;
   15.11  
   15.12  section "eta, subst and free";
    16.1 --- a/src/HOL/Lambda/InductTermi.ML	Tue Jan 19 11:16:39 1999 +0100
    16.2 +++ b/src/HOL/Lambda/InductTermi.ML	Tue Jan 19 11:18:11 1999 +0100
    16.3 @@ -43,48 +43,27 @@
    16.4  
    16.5  (*** Every terminating term is in IT ***)
    16.6  
    16.7 -val IT_cases = map (IT.mk_cases
    16.8 - ([Var_apps_eq_Var_apps_conv, Abs_eq_apps_conv, apps_eq_Abs_conv,
    16.9 -   Abs_apps_eq_Abs_apps_conv,
   16.10 -   Var_apps_neq_Abs_apps, Var_apps_neq_Abs_apps RS not_sym,
   16.11 -   hd(tl(get_thms List.thy "foldl.simps")) RS sym ]
   16.12 -  @ dB.simps @ list.simps))
   16.13 -    ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"];
   16.14 +Addsimps [Var_apps_neq_Abs_apps RS not_sym];
   16.15 +
   16.16 +Goal "Var n $$ ss ~= Abs r $ s $$ ts";
   16.17 +by (simp_tac (simpset() addsimps [foldl_Cons RS sym] 
   16.18 +	                delsimps [foldl_Cons]) 1);
   16.19 +qed "Var_apps_neq_Abs_app_apps";
   16.20 +Addsimps [Var_apps_neq_Abs_app_apps,
   16.21 +	  Var_apps_neq_Abs_app_apps RS not_sym];
   16.22 +
   16.23 +
   16.24 +Goal "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r=r' & s=s' & ss=ss')";
   16.25 +by (simp_tac (simpset() addsimps [foldl_Cons RS sym] 
   16.26 +	                delsimps [foldl_Cons]) 1);
   16.27 +qed "Abs_apps_eq_Abs_app_apps";
   16.28 +Addsimps [Abs_apps_eq_Abs_app_apps];
   16.29 +
   16.30 +val IT_cases = 
   16.31 +    map IT.mk_cases
   16.32 +        ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"];
   16.33  AddSEs IT_cases;
   16.34  
   16.35 -(* Turned out to be redundant:
   16.36 -Goal "t : termi beta ==> \
   16.37 -\     !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)";
   16.38 -by (etac acc_induct 1);
   16.39 -by (force_tac (claset()
   16.40 -     addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1);
   16.41 -val lemma = result();
   16.42 -
   16.43 -Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)";
   16.44 -by (dtac lemma 1);
   16.45 -by (Blast_tac 1);
   16.46 -qed "apps_in_termi_betaD";
   16.47 -
   16.48 -Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta";
   16.49 -by (etac acc_induct 1);
   16.50 -by (force_tac (claset() addIs [accI],simpset()) 1);
   16.51 -val lemma = result();
   16.52 -
   16.53 -Goal "Abs r : termi beta ==> r : termi beta";
   16.54 -by (dtac lemma 1);
   16.55 -by (Blast_tac 1);
   16.56 -qed "Abs_in_termi_betaD";
   16.57 -
   16.58 -Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta";
   16.59 -by (etac acc_induct 1);
   16.60 -by (force_tac (claset() addIs [accI],simpset()) 1);
   16.61 -val lemma = result();
   16.62 -
   16.63 -Goal "r$s : termi beta ==> r : termi beta & s : termi beta";
   16.64 -by (dtac lemma 1);
   16.65 -by (Blast_tac 1);
   16.66 -qed "App_in_termi_betaD";
   16.67 -*)
   16.68  
   16.69  Goal "r : termi beta ==> r : IT";
   16.70  by (etac acc_induct 1);
    17.1 --- a/src/HOL/Lambda/Lambda.ML	Tue Jan 19 11:16:39 1999 +0100
    17.2 +++ b/src/HOL/Lambda/Lambda.ML	Tue Jan 19 11:18:11 1999 +0100
    17.3 @@ -8,8 +8,7 @@
    17.4  
    17.5  (*** Lambda ***)
    17.6  
    17.7 -val beta_cases = map (beta.mk_cases dB.simps)
    17.8 -    ["Var i -> t", "Abs r -> s", "s $ t -> u"];
    17.9 +val beta_cases = map beta.mk_cases ["Var i -> t", "Abs r -> s", "s $ t -> u"];
   17.10  AddSEs beta_cases;
   17.11  
   17.12  Delsimps [subst_Var];
    18.1 --- a/src/HOL/Lambda/ParRed.ML	Tue Jan 19 11:16:39 1999 +0100
    18.2 +++ b/src/HOL/Lambda/ParRed.ML	Tue Jan 19 11:18:11 1999 +0100
    18.3 @@ -7,13 +7,15 @@
    18.4  confluence of beta.
    18.5  *)
    18.6  
    18.7 -open ParRed;
    18.8 -
    18.9  Addsimps par_beta.intrs;
   18.10  
   18.11 -val par_beta_cases = map (par_beta.mk_cases dB.simps)
   18.12 -    ["Var n => t", "Abs s => Abs t",
   18.13 -     "(Abs s) $ t => u", "s $ t => u", "Abs s => t"];
   18.14 +val par_beta_cases = 
   18.15 +    map par_beta.mk_cases
   18.16 +       ["Var n => t", 
   18.17 +	"Abs s => Abs t",
   18.18 +	"(Abs s) $ t => u", 
   18.19 +	"s $ t => u", 
   18.20 +	"Abs s => t"];
   18.21  
   18.22  AddSIs par_beta.intrs;
   18.23  AddSEs par_beta_cases;
    19.1 --- a/src/HOL/List.ML	Tue Jan 19 11:16:39 1999 +0100
    19.2 +++ b/src/HOL/List.ML	Tue Jan 19 11:18:11 1999 +0100
    19.3 @@ -32,7 +32,7 @@
    19.4  by (REPEAT (ares_tac basic_monos 1));
    19.5  qed "lists_mono";
    19.6  
    19.7 -val listsE = lists.mk_cases list.simps  "x#l : lists A";
    19.8 +val listsE = lists.mk_cases "x#l : lists A";
    19.9  AddSEs [listsE];
   19.10  AddSIs lists.intrs;
   19.11  
    20.1 --- a/src/HOL/List.thy	Tue Jan 19 11:16:39 1999 +0100
    20.2 +++ b/src/HOL/List.thy	Tue Jan 19 11:18:11 1999 +0100
    20.3 @@ -114,8 +114,8 @@
    20.4    "filter P [] = []"
    20.5    "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
    20.6  primrec
    20.7 -  "foldl f a [] = a"
    20.8 -  "foldl f a (x#xs) = foldl f (f a x) xs"
    20.9 +  foldl_Nil  "foldl f a [] = a"
   20.10 +  foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
   20.11  primrec
   20.12    "concat([]) = []"
   20.13    "concat(x#xs) = x @ concat(xs)"
    21.1 --- a/src/HOL/MiniML/W.ML	Tue Jan 19 11:16:39 1999 +0100
    21.2 +++ b/src/HOL/MiniML/W.ML	Tue Jan 19 11:18:11 1999 +0100
    21.3 @@ -6,16 +6,17 @@
    21.4  Correctness and completeness of type inference algorithm W
    21.5  *)
    21.6  
    21.7 -open W;
    21.8 -
    21.9  Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
   21.10  
   21.11 -val has_type_casesE = map(has_type.mk_cases expr.simps)
   21.12 -        [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ];
   21.13 +val has_type_casesE = 
   21.14 +    map has_type.mk_cases
   21.15 +	[" A |- Var n :: t",
   21.16 +	 " A |- Abs e :: t",
   21.17 +	 "A |- App e1 e2 ::t",
   21.18 +	 "A |- LET e1 e2 ::t" ];
   21.19  
   21.20  (* the resulting type variable is always greater or equal than the given one *)
   21.21 -Goal
   21.22 -        "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
   21.23 +Goal "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
   21.24  by (induct_tac "e" 1);
   21.25  (* case Var(n) *)
   21.26  by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   21.27 @@ -32,8 +33,7 @@
   21.28  
   21.29  Addsimps [W_var_ge];
   21.30  
   21.31 -Goal
   21.32 -        "Some (S,t,m) = W e A n ==> n<=m";
   21.33 +Goal "Some (S,t,m) = W e A n ==> n<=m";
   21.34  by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   21.35  qed "W_var_geD";
   21.36  
   21.37 @@ -67,8 +67,7 @@
   21.38  Addsimps [new_tv_bound_typ_inst_sch];
   21.39  
   21.40  (* resulting type variable is new *)
   21.41 -Goal
   21.42 -     "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
   21.43 +Goal "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
   21.44  \                 new_tv m S & new_tv m t";
   21.45  by (induct_tac "e" 1);
   21.46  (* case Var n *)
   21.47 @@ -163,8 +162,7 @@
   21.48  
   21.49  Addsimps [free_tv_bound_typ_inst1];
   21.50  
   21.51 -Goal
   21.52 -     "!n A S t m v. W e A n = Some (S,t,m) -->            \
   21.53 +Goal "!n A S t m v. W e A n = Some (S,t,m) -->            \
   21.54  \         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
   21.55  by (induct_tac "e" 1);
   21.56  (* case Var n *)
   21.57 @@ -259,8 +257,7 @@
   21.58  val weaken_not_elem_A_minus_B = result();
   21.59  
   21.60  (* correctness of W with respect to has_type *)
   21.61 -Goal
   21.62 -        "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
   21.63 +Goal "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
   21.64  by (induct_tac "e" 1);
   21.65  (* case Var n *)
   21.66  by (Asm_full_simp_tac 1);
   21.67 @@ -380,8 +377,7 @@
   21.68  qed_spec_mp "W_correct_lemma";
   21.69  
   21.70  (* Completeness of W w.r.t. has_type *)
   21.71 -Goal
   21.72 - "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
   21.73 +Goal "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
   21.74  \             (? S t. (? m. W e A n = Some (S,t,m)) &  \
   21.75  \                     (? R. $S' A = $R ($S A) & t' = $R t))";
   21.76  by (induct_tac "e" 1);
   21.77 @@ -554,8 +550,7 @@
   21.78  by (simp_tac (simpset() addsimps [o_def,subst_comp_scheme_list RS sym]) 1);
   21.79  qed_spec_mp "W_complete_lemma";
   21.80  
   21.81 -Goal
   21.82 - "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
   21.83 +Goal "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
   21.84  \                                 (? R. t' = $ R t))";
   21.85  by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
   21.86                  W_complete_lemma 1);
    22.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jan 19 11:16:39 1999 +0100
    22.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jan 19 11:18:11 1999 +0100
    22.3 @@ -34,13 +34,13 @@
    22.4      term list -> thm list -> thm list -> theory -> theory *
    22.5        {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
    22.6         intrs:thm list,
    22.7 -       mk_cases:thm list -> string -> thm, mono:thm,
    22.8 +       mk_cases:string -> thm, mono:thm,
    22.9         unfold:thm}
   22.10    val add_inductive : bool -> bool -> string list -> string list
   22.11      -> xstring list -> xstring list -> theory -> theory *
   22.12        {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
   22.13         intrs:thm list,
   22.14 -       mk_cases:thm list -> string -> thm, mono:thm,
   22.15 +       mk_cases:string -> thm, mono:thm,
   22.16         unfold:thm}
   22.17  end;
   22.18  
   22.19 @@ -289,21 +289,21 @@
   22.20    the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   22.21    for inference systems.
   22.22   *)
   22.23 -fun con_elim_tac simps =
   22.24 +fun con_elim_tac ss =
   22.25    let val elim_tac = REPEAT o (eresolve_tac elim_rls)
   22.26    in ALLGOALS(EVERY'[elim_tac,
   22.27 -                 asm_full_simp_tac (simpset_of NatDef.thy addsimps simps),
   22.28 -                 elim_tac,
   22.29 -                 REPEAT o bound_hyp_subst_tac])
   22.30 +		     asm_full_simp_tac ss,
   22.31 +		     elim_tac,
   22.32 +		     REPEAT o bound_hyp_subst_tac])
   22.33       THEN prune_params_tac
   22.34    end;
   22.35  
   22.36  (*String s should have the form t:Si where Si is an inductive set*)
   22.37 -fun mk_cases elims simps s =
   22.38 -  let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT));
   22.39 -      val elims' = map (try (fn r =>
   22.40 -        rule_by_tactic (con_elim_tac simps) (prem RS r) |> standard)) elims
   22.41 -  in case find_first is_some elims' of
   22.42 +fun mk_cases elims s =
   22.43 +  let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT))
   22.44 +      fun mk_elim rl = rule_by_tactic (con_elim_tac (simpset())) (prem RS rl) 
   22.45 +	               |> standard
   22.46 +  in case find_first is_some (map (try mk_elim) elims) of
   22.47         Some (Some r) => r
   22.48       | None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")
   22.49    end;
    23.1 --- a/src/HOL/W0/W.ML	Tue Jan 19 11:16:39 1999 +0100
    23.2 +++ b/src/HOL/W0/W.ML	Tue Jan 19 11:18:11 1999 +0100
    23.3 @@ -36,7 +36,7 @@
    23.4  by (asm_full_simp_tac (simpset() addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
    23.5  qed_spec_mp "W_correct";
    23.6  
    23.7 -val has_type_casesE = map(has_type.mk_cases expr.simps)
    23.8 +val has_type_casesE = map has_type.mk_cases
    23.9          [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
   23.10  
   23.11  (* the resulting type variable is always greater or equal than the given one *)
    24.1 --- a/src/ZF/Coind/ECR.ML	Tue Jan 19 11:16:39 1999 +0100
    24.2 +++ b/src/ZF/Coind/ECR.ML	Tue Jan 19 11:18:11 1999 +0100
    24.3 @@ -24,11 +24,9 @@
    24.4  
    24.5  (* Specialised elimination rules *)
    24.6  
    24.7 -val htr_constE = 
    24.8 -  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_const(c),t>:HasTyRel");
    24.9 +val htr_constE = HasTyRel.mk_cases "<v_const(c),t>:HasTyRel";
   24.10  
   24.11 -val htr_closE =
   24.12 -  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_clos(x,e,ve),t>:HasTyRel");
   24.13 +val htr_closE = HasTyRel.mk_cases "<v_clos(x,e,ve),t>:HasTyRel";
   24.14  
   24.15  (* Classical reasoning sets *)
   24.16  
    25.1 --- a/src/ZF/Coind/MT.ML	Tue Jan 19 11:16:39 1999 +0100
    25.2 +++ b/src/ZF/Coind/MT.ML	Tue Jan 19 11:18:11 1999 +0100
    25.3 @@ -55,7 +55,7 @@
    25.4  by (eres_inst_tac [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")] 
    25.5      (SigmaD1 RS te_owrE) 1);
    25.6  by (assume_tac 1);
    25.7 -by (rtac ElabRel.elab_fnI 1);
    25.8 +by (rtac ElabRel.fnI 1);
    25.9  by clean_tac;
   25.10  by (Asm_simp_tac 1);
   25.11  by (stac ve_dom_owr 1);
   25.12 @@ -78,8 +78,7 @@
   25.13  qed "consistency_fix";
   25.14  
   25.15  
   25.16 -Goal
   25.17 -   "[| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
   25.18 +Goal "[| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
   25.19  \     <ve,e1,v_const(c1)>:EvalRel;                      \
   25.20  \     ALL t te.                                         \
   25.21  \       hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
   25.22 @@ -93,25 +92,24 @@
   25.23  by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
   25.24  qed "consistency_app1";
   25.25  
   25.26 -Goal
   25.27 -   "[| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;  \
   25.28 -\      <ve,e1,v_clos(xm,em,vem)>:EvalRel;       \
   25.29 -\      ALL t te.                                \
   25.30 -\        hastyenv(ve,te) -->                    \
   25.31 -\        <te,e1,t>:ElabRel -->                  \
   25.32 -\        <v_clos(xm,em,vem),t>:HasTyRel;        \
   25.33 -\      <ve,e2,v2>:EvalRel;                      \
   25.34 -\      ALL t te.                                \
   25.35 -\        hastyenv(ve,te) -->                    \
   25.36 -\        <te,e2,t>:ElabRel -->                  \
   25.37 -\        <v2,t>:HasTyRel;                       \
   25.38 -\      <ve_owr(vem,xm,v2),em,v>:EvalRel;        \
   25.39 -\      ALL t te.                                \
   25.40 -\        hastyenv(ve_owr(vem,xm,v2),te) -->     \
   25.41 -\        <te,em,t>:ElabRel -->                  \
   25.42 -\        <v,t>:HasTyRel;                        \
   25.43 -\      hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==>      \
   25.44 -\   <v,t>:HasTyRel ";
   25.45 +Goal "[| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;  \
   25.46 +\        <ve,e1,v_clos(xm,em,vem)>:EvalRel;       \
   25.47 +\        ALL t te.                                \
   25.48 +\          hastyenv(ve,te) -->                    \
   25.49 +\          <te,e1,t>:ElabRel -->                  \
   25.50 +\          <v_clos(xm,em,vem),t>:HasTyRel;        \
   25.51 +\        <ve,e2,v2>:EvalRel;                      \
   25.52 +\        ALL t te.                                \
   25.53 +\          hastyenv(ve,te) -->                    \
   25.54 +\          <te,e2,t>:ElabRel -->                  \
   25.55 +\          <v2,t>:HasTyRel;                       \
   25.56 +\        <ve_owr(vem,xm,v2),em,v>:EvalRel;        \
   25.57 +\        ALL t te.                                \
   25.58 +\          hastyenv(ve_owr(vem,xm,v2),te) -->     \
   25.59 +\          <te,em,t>:ElabRel -->                  \
   25.60 +\          <v,t>:HasTyRel;                        \
   25.61 +\        hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==>      \
   25.62 +\     <v,t>:HasTyRel ";
   25.63  by (etac elab_appE 1);
   25.64  by (dtac (spec RS spec RS mp RS mp) 1);
   25.65  by (assume_tac 1);
   25.66 @@ -121,8 +119,8 @@
   25.67  by (assume_tac 1);
   25.68  by (etac htr_closE 1);
   25.69  by (etac elab_fnE 1);
   25.70 -by (rewrite_tac Ty.con_defs);
   25.71 -by Safe_tac;
   25.72 +by (Full_simp_tac 1);
   25.73 +by (Clarify_tac 1);
   25.74  by (dtac (spec RS spec RS mp RS mp) 1);
   25.75  by (assume_tac 3);
   25.76  by (assume_tac 2);
   25.77 @@ -130,33 +128,24 @@
   25.78  by (assume_tac 1);
   25.79  by (assume_tac 1);
   25.80  by (assume_tac 2);
   25.81 -by (simp_tac (simpset() addsimps [hastyenv_def]) 1);
   25.82 +by (asm_simp_tac (simpset() addsimps [hastyenv_def]) 1);
   25.83  by (Fast_tac 1);
   25.84  qed "consistency_app2";
   25.85  
   25.86 -fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac)); 
   25.87 -
   25.88  Goal "<ve,e,v>:EvalRel ==>         \
   25.89  \       (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
   25.90  by (etac EvalRel.induct 1);
   25.91 -by (safe_tac ZF_cs);
   25.92 -by (mt_cases_tac consistency_const);
   25.93 -by (mt_cases_tac consistency_var);
   25.94 -by (mt_cases_tac consistency_fn);
   25.95 -by (mt_cases_tac consistency_fix);
   25.96 -by (mt_cases_tac consistency_app1);
   25.97 -by (mt_cases_tac consistency_app2);
   25.98 +by (blast_tac (claset() addIs [consistency_app2]) 6);
   25.99 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1])));
  25.100  qed "consistency";
  25.101  
  25.102  
  25.103 -Goal
  25.104 -  "[| ve:ValEnv; te:TyEnv;              \
  25.105 -\     isofenv(ve,te);                   \
  25.106 -\     <ve,e,v_const(c)>:EvalRel;        \
  25.107 -\     <te,e,t>:ElabRel                  \
  25.108 -\  |] ==>                               \
  25.109 -\  isof(c,t)";
  25.110 -by (rtac (htr_constE) 1);
  25.111 +Goal "[| ve:ValEnv; te:TyEnv;              \
  25.112 +\        isofenv(ve,te);                   \
  25.113 +\        <ve,e,v_const(c)>:EvalRel;        \
  25.114 +\        <te,e,t>:ElabRel                  \
  25.115 +\     |] ==> isof(c,t)";
  25.116 +by (rtac htr_constE 1);
  25.117  by (dtac consistency 1);
  25.118  by (fast_tac (claset() addSIs [basic_consistency_lem]) 1);
  25.119  by (assume_tac 1);
    26.1 --- a/src/ZF/Coind/Static.ML	Tue Jan 19 11:16:39 1999 +0100
    26.2 +++ b/src/ZF/Coind/Static.ML	Tue Jan 19 11:18:11 1999 +0100
    26.3 @@ -4,27 +4,22 @@
    26.4      Copyright   1995  University of Cambridge
    26.5  *)
    26.6  
    26.7 -open BCR Static;
    26.8 +val elab_constE	= ElabRel.mk_cases "<te,e_const(c),t>:ElabRel";
    26.9  
   26.10 -val elab_constE = 
   26.11 -  ElabRel.mk_cases Exp.con_defs "<te,e_const(c),t>:ElabRel";
   26.12 +val elab_varE 	= ElabRel.mk_cases "<te,e_var(x),t>:ElabRel";
   26.13  
   26.14 -val elab_varE =
   26.15 -  ElabRel.mk_cases Exp.con_defs "<te,e_var(x),t>:ElabRel";
   26.16 +val elab_fnE 	= ElabRel.mk_cases "<te,e_fn(x,e),t>:ElabRel";
   26.17  
   26.18 -val elab_fnE =
   26.19 -  ElabRel.mk_cases Exp.con_defs "<te,e_fn(x,e),t>:ElabRel";
   26.20 +val elab_fixE 	= ElabRel.mk_cases "<te,e_fix(f,x,e),t>:ElabRel";
   26.21 +
   26.22 +val elab_appE 	= ElabRel.mk_cases "<te,e_app(e1,e2),t>:ElabRel";
   26.23  
   26.24 -val elab_fixE =
   26.25 -  ElabRel.mk_cases Exp.con_defs "<te,e_fix(f,x,e),t>:ElabRel";
   26.26 +AddSEs [elab_constE, elab_varE, elab_fixE];
   26.27  
   26.28 -val elab_appE = 
   26.29 -  ElabRel.mk_cases Exp.con_defs "<te,e_app(e1,e2),t>:ElabRel";
   26.30 +AddSIs [ElabRel.constI, ElabRel.varI, ElabRel.fnI, ElabRel.fixI];
   26.31  
   26.32 -let open ElabRel in 
   26.33 -claset_ref() := claset() addSIs [elab_constI,elab_varI,elab_fnI,elab_fixI]
   26.34 -                  addSEs [elab_constE,elab_varE,elab_fixE]
   26.35 -		  addIs [elab_appI]
   26.36 -		  addEs [elab_appE,elab_fnE]
   26.37 -		  addDs [ElabRel.dom_subset RS subsetD]
   26.38 -end;
   26.39 +AddIs  [ElabRel.appI];
   26.40 +
   26.41 +AddEs [elab_appE, elab_fnE];
   26.42 +
   26.43 +AddDs [ElabRel.dom_subset RS subsetD];
    27.1 --- a/src/ZF/Coind/Static.thy	Tue Jan 19 11:16:39 1999 +0100
    27.2 +++ b/src/ZF/Coind/Static.thy	Tue Jan 19 11:18:11 1999 +0100
    27.3 @@ -6,26 +6,26 @@
    27.4  
    27.5  Static = BCR +
    27.6  
    27.7 -consts
    27.8 -  ElabRel :: i
    27.9 +consts  ElabRel :: i
   27.10 +
   27.11  inductive
   27.12    domains "ElabRel" <= "TyEnv * Exp * Ty"
   27.13    intrs
   27.14 -    elab_constI
   27.15 +    constI
   27.16        " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   
   27.17         <te,e_const(c),t>:ElabRel "
   27.18 -    elab_varI
   27.19 +    varI
   27.20        " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   
   27.21         <te,e_var(x),te_app(te,x)>:ElabRel "
   27.22 -    elab_fnI
   27.23 +    fnI
   27.24        " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   
   27.25            <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   
   27.26         <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
   27.27 -    elab_fixI
   27.28 +    fixI
   27.29        " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   
   27.30            <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   
   27.31         <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
   27.32 -    elab_appI
   27.33 +    appI
   27.34        " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   
   27.35            <te,e1,t_fun(t1,t2)>:ElabRel;   
   27.36            <te,e2,t1>:ElabRel |] ==>   
    28.1 --- a/src/ZF/Coind/Types.ML	Tue Jan 19 11:16:39 1999 +0100
    28.2 +++ b/src/ZF/Coind/Types.ML	Tue Jan 19 11:18:11 1999 +0100
    28.3 @@ -4,10 +4,7 @@
    28.4      Copyright   1995  University of Cambridge
    28.5  *)
    28.6  
    28.7 -open Types;
    28.8 -
    28.9 -val te_owrE = 
   28.10 -  TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv";
   28.11 +val te_owrE = TyEnv.mk_cases "te_owr(te,f,t):TyEnv";
   28.12  
   28.13  Goal "te_app(te_owr(te,x,t),x) = t";
   28.14  by (Simp_tac 1);
    29.1 --- a/src/ZF/Datatype.ML	Tue Jan 19 11:16:39 1999 +0100
    29.2 +++ b/src/ZF/Datatype.ML	Tue Jan 19 11:18:11 1999 +0100
    29.3 @@ -47,3 +47,59 @@
    29.4  			  and Ind_Package = CoInd_Package
    29.5  			  and Datatype_Arg = CoData_Arg);
    29.6  
    29.7 +
    29.8 +
    29.9 +(*Simproc for freeness reasoning: compare datatype constructors for equality*)
   29.10 +structure DataFree =
   29.11 +struct
   29.12 +  (*prove while suppressing timing information*)
   29.13 +  fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
   29.14 +
   29.15 +  val trace = ref false;
   29.16 +
   29.17 +  fun mk_new ([],[]) = Const("True",FOLogic.oT)
   29.18 +    | mk_new (largs,rargs) =
   29.19 +	fold_bal (app FOLogic.conj) 
   29.20 +		 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
   29.21 +
   29.22 +
   29.23 + fun proc sg _ old =
   29.24 +   let val _ = if !trace then writeln ("data_free: OLD = " ^ 
   29.25 +				       string_of_cterm (cterm_of sg old))
   29.26 +	       else ()
   29.27 +       val (lhs,rhs) = FOLogic.dest_eq old
   29.28 +       val (lhead, largs) = strip_comb lhs
   29.29 +       and (rhead, rargs) = strip_comb rhs
   29.30 +       val lname = #1 (dest_Const lhead)
   29.31 +       and rname = #1 (dest_Const rhead)
   29.32 +       val lcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, lname))
   29.33 +       and rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname))
   29.34 +       val new = 
   29.35 +	   if #big_rec_name lcon_info = #big_rec_name rcon_info 
   29.36 +	       andalso not (null (#free_iffs lcon_info)) then
   29.37 +	       if lname = rname then mk_new (largs, rargs)
   29.38 +	       else Const("False",FOLogic.oT)
   29.39 +	   else raise Match
   29.40 +       val _ = if !trace then 
   29.41 +		 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
   29.42 +	       else ()
   29.43 +       val ct = Thm.cterm_of sg (Logic.mk_equals (old, new))
   29.44 +       val thm = prove ct 
   29.45 +		   (fn _ => [rtac iff_reflection 1,
   29.46 +			     simp_tac (simpset_of Datatype.thy
   29.47 +  				          addsimps #free_iffs lcon_info) 1])
   29.48 +	 handle ERROR =>
   29.49 +	 error("data_free simproc:\nfailed to prove " ^
   29.50 +	       string_of_cterm ct)
   29.51 +   in Some thm end
   29.52 +   handle _ => None;
   29.53 +
   29.54 +
   29.55 + val conv = 
   29.56 +     Simplifier.mk_simproc "data_free"
   29.57 +       [Thm.read_cterm (sign_of ZF.thy) ("(x::i) = y", FOLogic.oT)]
   29.58 +       proc;
   29.59 +end;
   29.60 +
   29.61 +
   29.62 +Addsimprocs [DataFree.conv];
    30.1 --- a/src/ZF/IMP/Com.ML	Tue Jan 19 11:16:39 1999 +0100
    30.2 +++ b/src/ZF/IMP/Com.ML	Tue Jan 19 11:18:11 1999 +0100
    30.3 @@ -4,8 +4,6 @@
    30.4      Copyright   1994 TUM
    30.5  *)
    30.6  
    30.7 -open Com;
    30.8 -
    30.9  val type_cs = claset() addSDs [evala.dom_subset RS subsetD,
   30.10  			      evalb.dom_subset RS subsetD,
   30.11  			      evalc.dom_subset RS subsetD];
   30.12 @@ -42,8 +40,8 @@
   30.13  
   30.14  val aexp_elim_cases = 
   30.15     [
   30.16 -    evala.mk_cases aexp.con_defs "<N(n),sigma> -a-> i",
   30.17 -    evala.mk_cases aexp.con_defs "<X(x),sigma> -a-> i",
   30.18 -    evala.mk_cases aexp.con_defs "<Op1(f,e),sigma> -a-> i",
   30.19 -    evala.mk_cases aexp.con_defs "<Op2(f,a1,a2),sigma>  -a-> i"
   30.20 +    evala.mk_cases "<N(n),sigma> -a-> i",
   30.21 +    evala.mk_cases "<X(x),sigma> -a-> i",
   30.22 +    evala.mk_cases "<Op1(f,e),sigma> -a-> i",
   30.23 +    evala.mk_cases "<Op2(f,a1,a2),sigma>  -a-> i"
   30.24     ];
    31.1 --- a/src/ZF/IMP/Equiv.ML	Tue Jan 19 11:16:39 1999 +0100
    31.2 +++ b/src/ZF/IMP/Equiv.ML	Tue Jan 19 11:18:11 1999 +0100
    31.3 @@ -20,12 +20,12 @@
    31.4  
    31.5  val bexp_elim_cases = 
    31.6     [
    31.7 -    evalb.mk_cases bexp.con_defs "<true,sigma> -b-> x",
    31.8 -    evalb.mk_cases bexp.con_defs "<false,sigma> -b-> x",
    31.9 -    evalb.mk_cases bexp.con_defs "<ROp(f,a0,a1),sigma> -b-> x",
   31.10 -    evalb.mk_cases bexp.con_defs "<noti(b),sigma> -b-> x",
   31.11 -    evalb.mk_cases bexp.con_defs "<b0 andi b1,sigma> -b-> x",
   31.12 -    evalb.mk_cases bexp.con_defs "<b0 ori b1,sigma> -b-> x"
   31.13 +    evalb.mk_cases "<true,sigma> -b-> x",
   31.14 +    evalb.mk_cases "<false,sigma> -b-> x",
   31.15 +    evalb.mk_cases "<ROp(f,a0,a1),sigma> -b-> x",
   31.16 +    evalb.mk_cases "<noti(b),sigma> -b-> x",
   31.17 +    evalb.mk_cases "<b0 andi b1,sigma> -b-> x",
   31.18 +    evalb.mk_cases "<b0 ori b1,sigma> -b-> x"
   31.19     ];
   31.20  
   31.21  
    32.1 --- a/src/ZF/List.ML	Tue Jan 19 11:16:39 1999 +0100
    32.2 +++ b/src/ZF/List.ML	Tue Jan 19 11:18:11 1999 +0100
    32.3 @@ -9,7 +9,7 @@
    32.4  (*** Aspects of the datatype definition ***)
    32.5  
    32.6  (*An elimination rule, for type-checking*)
    32.7 -val ConsE = list.mk_cases list.con_defs "Cons(a,l) : list(A)";
    32.8 +val ConsE = list.mk_cases "Cons(a,l) : list(A)";
    32.9  
   32.10  (*Proving freeness results*)
   32.11  val Cons_iff     = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
    33.1 --- a/src/ZF/Resid/Redex.ML	Tue Jan 19 11:16:39 1999 +0100
    33.2 +++ b/src/ZF/Resid/Redex.ML	Tue Jan 19 11:18:11 1999 +0100
    33.3 @@ -12,10 +12,10 @@
    33.4  (*    Specialisation of comp-rules                                           *)
    33.5  (* ------------------------------------------------------------------------- *)
    33.6  
    33.7 -val compD1 =Scomp.dom_subset RS subsetD RS SigmaD1;
    33.8 -val compD2 =Scomp.dom_subset RS subsetD RS SigmaD2;
    33.9 +val compD1 = Scomp.dom_subset RS subsetD RS SigmaD1;
   33.10 +val compD2 = Scomp.dom_subset RS subsetD RS SigmaD2;
   33.11  
   33.12 -val regD =Sreg.dom_subset RS subsetD;
   33.13 +val regD = Sreg.dom_subset RS subsetD;
   33.14  
   33.15  (* ------------------------------------------------------------------------- *)
   33.16  (*    Equality rules for union                                               *)
   33.17 @@ -29,8 +29,7 @@
   33.18  by (asm_simp_tac (simpset() addsimps [union_def]) 1);
   33.19  qed "union_Fun";
   33.20   
   33.21 -Goal
   33.22 - "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
   33.23 +Goal "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
   33.24  \     App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
   33.25  by (asm_simp_tac (simpset() addsimps [union_def]) 1);
   33.26  qed "union_App";
   33.27 @@ -42,17 +41,16 @@
   33.28  	   union_App,union_Fun,union_Var,compD2,compD1,regD]);
   33.29  
   33.30  AddIs Scomp.intrs;
   33.31 -AddSEs [Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))",
   33.32 -	Sreg.mk_cases redexes.con_defs "regular(Fun(b))",
   33.33 -	Sreg.mk_cases redexes.con_defs "regular(Var(b))",
   33.34 -	Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)",
   33.35 -	Scomp.mk_cases redexes.con_defs "u ~ Fun(t)",
   33.36 -	Scomp.mk_cases redexes.con_defs "u ~ Var(n)",
   33.37 -	Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)",
   33.38 -	Scomp.mk_cases redexes.con_defs "Fun(t) ~ v",
   33.39 -	Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v",
   33.40 -	Scomp.mk_cases redexes.con_defs "Var(n) ~ u"
   33.41 -	];
   33.42 +AddSEs [Sreg.mk_cases "regular(App(b,f,a))",
   33.43 +	Sreg.mk_cases "regular(Fun(b))",
   33.44 +	Sreg.mk_cases "regular(Var(b))",
   33.45 +	Scomp.mk_cases "Fun(u) ~ Fun(t)",
   33.46 +	Scomp.mk_cases "u ~ Fun(t)",
   33.47 +	Scomp.mk_cases "u ~ Var(n)",
   33.48 +	Scomp.mk_cases "u ~ App(b,t,a)",
   33.49 +	Scomp.mk_cases "Fun(t) ~ v",
   33.50 +	Scomp.mk_cases "App(b,f,a) ~ v",
   33.51 +	Scomp.mk_cases "Var(n) ~ u"];
   33.52  
   33.53  
   33.54  
    34.1 --- a/src/ZF/Resid/Reduction.ML	Tue Jan 19 11:16:39 1999 +0100
    34.2 +++ b/src/ZF/Resid/Reduction.ML	Tue Jan 19 11:18:11 1999 +0100
    34.3 @@ -5,9 +5,6 @@
    34.4      Logic Image: ZF
    34.5  *)
    34.6  
    34.7 -open Reduction;
    34.8 -
    34.9 -
   34.10  (* ------------------------------------------------------------------------- *)
   34.11  (*     Setting up rulelists for reduction                                    *)
   34.12  (* ------------------------------------------------------------------------- *)
   34.13 @@ -25,7 +22,7 @@
   34.14  AddIs (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
   34.15         [Spar_red.one_step, lambda.dom_subset RS subsetD,
   34.16  	unmark_type]@lambda.intrs@bool_typechecks);
   34.17 -AddSEs [Spar_red1.mk_cases redexes.con_defs "Fun(t) =1=> Fun(u)"];
   34.18 +AddSEs [Spar_red1.mk_cases "Fun(t) =1=> Fun(u)"];
   34.19  
   34.20  Addsimps (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
   34.21  	  [Spar_red.one_step, substL_type, redD1, redD2, par_redD1, 
    35.1 --- a/src/ZF/Resid/Residuals.ML	Tue Jan 19 11:16:39 1999 +0100
    35.2 +++ b/src/ZF/Resid/Residuals.ML	Tue Jan 19 11:18:11 1999 +0100
    35.3 @@ -10,8 +10,7 @@
    35.4  (* ------------------------------------------------------------------------- *)
    35.5  
    35.6  AddIs (Sres.intrs @ redexes.intrs @ Sreg.intrs @ [subst_type]); 
    35.7 -AddSEs (redexes.free_SEs @
    35.8 -	(map (Sres.mk_cases redexes.con_defs) 
    35.9 +AddSEs (map Sres.mk_cases
   35.10  	     ["residuals(Var(n),Var(n),v)",
   35.11  	      "residuals(Fun(t),Fun(u),v)",
   35.12  	      "residuals(App(b, u1, u2), App(0, v1, v2),v)",
   35.13 @@ -21,19 +20,21 @@
   35.14  	      "residuals(App(b, u1, u2), w,v)",
   35.15  	      "residuals(u,Var(n),v)",
   35.16  	      "residuals(u,Fun(t),v)",
   35.17 -	      "residuals(w,App(b, u1, u2),v)"]) @
   35.18 -	(map (Ssub.mk_cases redexes.con_defs) 
   35.19 +	      "residuals(w,App(b, u1, u2),v)"]);
   35.20 +
   35.21 +AddSEs (map Ssub.mk_cases
   35.22  	     ["Var(n) <== u",
   35.23  	      "Fun(n) <== u",
   35.24  	      "u <== Fun(n)",
   35.25  	      "App(1,Fun(t),a) <== u",
   35.26 -	      "App(0,t,a) <== u"]) @
   35.27 -	[redexes.mk_cases redexes.con_defs "Fun(t):redexes"]);
   35.28 +	      "App(0,t,a) <== u"]);
   35.29 +
   35.30 +AddSEs [redexes.mk_cases "Fun(t):redexes"];
   35.31  
   35.32  Addsimps Sres.intrs;
   35.33 -val resD1 =Sres.dom_subset RS subsetD RS SigmaD1;
   35.34 -val resD2 =Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1;
   35.35 -val resD3 =Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2;
   35.36 +val resD1 = Sres.dom_subset RS subsetD RS SigmaD1;
   35.37 +val resD2 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1;
   35.38 +val resD3 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2;
   35.39  
   35.40  
   35.41  (* ------------------------------------------------------------------------- *)
   35.42 @@ -42,7 +43,7 @@
   35.43  
   35.44  Goal "residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w";
   35.45  by (etac Sres.induct 1);
   35.46 -by (ALLGOALS Fast_tac);
   35.47 +by (ALLGOALS Force_tac);
   35.48  qed_spec_mp "residuals_function";
   35.49  
   35.50  Goal "u~v ==> regular(v) --> (EX w. residuals(u,v,w))";
   35.51 @@ -81,7 +82,8 @@
   35.52  Goalw [res_func_def]
   35.53      "[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
   35.54  \           App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
   35.55 -by (blast_tac (claset() addSDs [comp_resfuncD]
   35.56 +by (blast_tac (claset() addSEs redexes.free_SEs
   35.57 +			addSDs [comp_resfuncD]
   35.58  			addIs [residuals_function]) 1);
   35.59  qed "res_redex";
   35.60  
   35.61 @@ -98,8 +100,6 @@
   35.62  	  lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type,
   35.63  	  subst_rec_preserve_reg];
   35.64  
   35.65 -Addsimps redexes.free_iffs;
   35.66 -
   35.67  
   35.68  (* ------------------------------------------------------------------------- *)
   35.69  (*     Commutation theorem                                                   *)
    36.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Jan 19 11:16:39 1999 +0100
    36.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Jan 19 11:18:11 1999 +0100
    36.3 @@ -380,6 +380,7 @@
    36.4          {big_rec_name = big_rec_name,
    36.5  	 constructors = constructors,
    36.6              (*let primrec handle definition by cases*)
    36.7 +	 free_iffs = free_iffs,
    36.8  	 rec_rewrites = (case recursor_eqns of
    36.9  			     [] => case_eqns | _ => recursor_eqns)};
   36.10  
    37.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Jan 19 11:16:39 1999 +0100
    37.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Jan 19 11:18:11 1999 +0100
    37.3 @@ -53,6 +53,7 @@
    37.4  type constructor_info =
    37.5    {big_rec_name : string,     (*name of the mutually recursive set*)
    37.6     constructors : term list,  (*the constructors, as Consts*)
    37.7 +   free_iffs    : thm list,   (*freeness simprules*)
    37.8     rec_rewrites : thm list};  (*recursor equations*)
    37.9  
   37.10  
   37.11 @@ -161,6 +162,9 @@
   37.12  	  {big_rec_name = big_rec_name,
   37.13  	   constructors = constructors,
   37.14  	      (*let primrec handle definition by cases*)
   37.15 +	   free_iffs = [],  (*thus we expect the necessary freeness rewrites
   37.16 +			      to be in the simpset already, as is the case for
   37.17 +			      Nat and disjoint sum*)
   37.18  	   rec_rewrites = (case recursor_eqns of
   37.19  			       [] => case_eqns | _ => recursor_eqns)};
   37.20  
    38.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Jan 19 11:16:39 1999 +0100
    38.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Jan 19 11:18:11 1999 +0100
    38.3 @@ -19,7 +19,7 @@
    38.4      dom_subset : thm,                  (*inclusion of recursive set in dom*)
    38.5      intrs      : thm list,             (*introduction rules*)
    38.6      elim       : thm,                  (*case analysis theorem*)
    38.7 -    mk_cases   : thm list -> string -> thm,    (*generates case theorems*)
    38.8 +    mk_cases   : string -> thm,        (*generates case theorems*)
    38.9      induct     : thm,                  (*main induction rule*)
   38.10      mutual_induct : thm};              (*mutual induction rule*)
   38.11  
   38.12 @@ -270,10 +270,10 @@
   38.13        the given defs.  Cannot simply use the local con_defs because  
   38.14        con_defs=[] for inference systems. 
   38.15      String s should have the form t:Si where Si is an inductive set*)
   38.16 -  fun mk_cases defs s = 
   38.17 -      rule_by_tactic (rewrite_goals_tac defs THEN 
   38.18 -		      basic_elim_tac THEN
   38.19 -		      fold_tac defs)
   38.20 +  fun mk_cases s = 
   38.21 +      rule_by_tactic (basic_elim_tac THEN
   38.22 +		      ALLGOALS Asm_full_simp_tac THEN 
   38.23 +		      basic_elim_tac)
   38.24  	 (assume_read (theory_of_thm elim) s
   38.25  	              (*Don't use thy1: it will be stale*)
   38.26  	  RS  elim)
    39.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Jan 19 11:16:39 1999 +0100
    39.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Jan 19 11:18:11 1999 +0100
    39.3 @@ -18,10 +18,8 @@
    39.4  
    39.5  exception RecError of string;
    39.6  
    39.7 -(* FIXME: move? *)
    39.8 -
    39.9 -fun dest_eq (Const ("Trueprop", _) $ (Const ("op =", _) $ lhs $ rhs)) = (lhs, rhs)
   39.10 -  | dest_eq t = raise TERM ("dest_eq", [t])
   39.11 +(*Remove outer Trueprop and equality sign*)
   39.12 +val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop;
   39.13  
   39.14  fun primrec_err s = error ("Primrec definition error:\n" ^ s);
   39.15  
   39.16 @@ -33,9 +31,10 @@
   39.17  (*rec_fn_opt records equations already noted for this function*)
   39.18  fun process_eqn thy (eq, rec_fn_opt) = 
   39.19    let
   39.20 -    val (lhs, rhs) = if null (term_vars eq) then
   39.21 -        dest_eq eq handle _ => raise RecError "not a proper equation"
   39.22 -      else raise RecError "illegal schematic variable(s)";
   39.23 +    val (lhs, rhs) = 
   39.24 +	if null (term_vars eq) then
   39.25 +	    dest_eqn eq handle _ => raise RecError "not a proper equation"
   39.26 +	else raise RecError "illegal schematic variable(s)";
   39.27  
   39.28      val (recfun, args) = strip_comb lhs;
   39.29      val (fname, ftype) = dest_Const recfun handle _ => 
   39.30 @@ -104,7 +103,7 @@
   39.31        | use_fabs t       = t
   39.32  
   39.33      val cnames         = map (#1 o dest_Const) constructors
   39.34 -    and recursor_pairs = map (dest_eq o concl_of) rec_rewrites
   39.35 +    and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites
   39.36  
   39.37      fun absterm (Free(a,T), body) = absfree (a,T,body)
   39.38        | absterm (t,body)          = Abs("rec", iT, abstract_over (t, body))
    40.1 --- a/src/ZF/ex/BT.ML	Tue Jan 19 11:16:39 1999 +0100
    40.2 +++ b/src/ZF/ex/BT.ML	Tue Jan 19 11:18:11 1999 +0100
    40.3 @@ -10,14 +10,14 @@
    40.4  
    40.5  Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
    40.6  by (induct_tac "l" 1);
    40.7 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs)));
    40.8 +by (ALLGOALS Asm_full_simp_tac);
    40.9  qed_spec_mp "Br_neq_left";
   40.10  
   40.11  (*Proving a freeness theorem*)
   40.12  val Br_iff = bt.mk_free "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'";
   40.13  
   40.14  (*An elimination rule, for type-checking*)
   40.15 -val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)";
   40.16 +val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
   40.17  
   40.18  (**  Lemmas to justify using "bt" in other recursive type definitions **)
   40.19  
    41.1 --- a/src/ZF/ex/CoUnit.ML	Tue Jan 19 11:16:39 1999 +0100
    41.2 +++ b/src/ZF/ex/CoUnit.ML	Tue Jan 19 11:18:11 1999 +0100
    41.3 @@ -10,10 +10,8 @@
    41.4    Report 334,  Cambridge University Computer Laboratory.  1994.
    41.5  *)
    41.6  
    41.7 -open CoUnit;
    41.8 -  
    41.9  (*USELESS because folding on Con(?xa) == ?xa fails*)
   41.10 -val ConE = counit.mk_cases counit.con_defs "Con(x) : counit";
   41.11 +val ConE = counit.mk_cases "Con(x) : counit";
   41.12  
   41.13  (*Proving freeness results*)
   41.14  val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y";
   41.15 @@ -33,7 +31,7 @@
   41.16    The resulting set is a singleton.
   41.17  *)
   41.18  
   41.19 -val Con2E = counit2.mk_cases counit2.con_defs "Con2(x,y) : counit2";
   41.20 +val Con2E = counit2.mk_cases "Con2(x,y) : counit2";
   41.21  
   41.22  (*Proving freeness results*)
   41.23  val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
    42.1 --- a/src/ZF/ex/Comb.ML	Tue Jan 19 11:16:39 1999 +0100
    42.2 +++ b/src/ZF/ex/Comb.ML	Tue Jan 19 11:18:11 1999 +0100
    42.3 @@ -15,8 +15,6 @@
    42.4  /usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
    42.5  *)
    42.6  
    42.7 -open Comb;
    42.8 -
    42.9  (*** Transitive closure preserves the Church-Rosser property ***)
   42.10  
   42.11  Goalw [diamond_def]
   42.12 @@ -39,7 +37,7 @@
   42.13  
   42.14  
   42.15  val [_,_,comb_Ap] = comb.intrs;
   42.16 -val Ap_E = comb.mk_cases comb.con_defs "p#q : comb";
   42.17 +val Ap_E = comb.mk_cases "p#q : comb";
   42.18  
   42.19  AddSIs comb.intrs;
   42.20  AddSEs comb.free_SEs;
   42.21 @@ -81,9 +79,9 @@
   42.22  (** Non-contraction results **)
   42.23  
   42.24  (*Derive a case for each combinator constructor*)
   42.25 -val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
   42.26 -val S_contractE = contract.mk_cases comb.con_defs "S -1-> r";
   42.27 -val Ap_contractE = contract.mk_cases comb.con_defs "p#q -1-> r";
   42.28 +val K_contractE = contract.mk_cases "K -1-> r";
   42.29 +val S_contractE = contract.mk_cases "S -1-> r";
   42.30 +val Ap_contractE = contract.mk_cases "p#q -1-> r";
   42.31  
   42.32  AddIs  [contract.Ap1, contract.Ap2];
   42.33  AddSEs [K_contractE, S_contractE, Ap_contractE];
   42.34 @@ -148,9 +146,9 @@
   42.35  qed "field_parcontract_eq";
   42.36  
   42.37  (*Derive a case for each combinator constructor*)
   42.38 -val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r";
   42.39 -val S_parcontractE = parcontract.mk_cases comb.con_defs "S =1=> r";
   42.40 -val Ap_parcontractE = parcontract.mk_cases comb.con_defs "p#q =1=> r";
   42.41 +val K_parcontractE = parcontract.mk_cases "K =1=> r";
   42.42 +val S_parcontractE = parcontract.mk_cases "S =1=> r";
   42.43 +val Ap_parcontractE = parcontract.mk_cases "p#q =1=> r";
   42.44  
   42.45  AddIs  parcontract.intrs;
   42.46  AddSEs [Ap_E, K_parcontractE, S_parcontractE, Ap_parcontractE];
    43.1 --- a/src/ZF/ex/Enum.ML	Tue Jan 19 11:16:39 1999 +0100
    43.2 +++ b/src/ZF/ex/Enum.ML	Tue Jan 19 11:18:11 1999 +0100
    43.3 @@ -8,9 +8,7 @@
    43.4  Can go up to at least 100 constructors, but it takes nearly 7 minutes...
    43.5  *)
    43.6  
    43.7 -open Enum;
    43.8 -
    43.9  Goal "C00 ~= C01";
   43.10 -by (simp_tac (simpset() addsimps enum.free_iffs) 1);
   43.11 +by (Simp_tac 1);
   43.12  result();
   43.13  
    44.1 --- a/src/ZF/ex/LList.ML	Tue Jan 19 11:16:39 1999 +0100
    44.2 +++ b/src/ZF/ex/LList.ML	Tue Jan 19 11:18:11 1999 +0100
    44.3 @@ -6,8 +6,9 @@
    44.4  Codatatype definition of Lazy Lists
    44.5  *)
    44.6  
    44.7 -open LList;
    44.8 -
    44.9 +(*These commands cause classical reasoning to regard the subset relation
   44.10 +  as primitive, not reducing it to membership*)
   44.11 +  
   44.12  Delrules [subsetI, subsetCE];
   44.13  AddSIs [subset_refl, cons_subsetI, subset_consI, 
   44.14  	Union_least, UN_least, Un_least, 
   44.15 @@ -15,7 +16,7 @@
   44.16  	Un_upper1, Un_upper2, Int_lower1, Int_lower2];
   44.17  
   44.18  (*An elimination rule, for type-checking*)
   44.19 -val LConsE = llist.mk_cases llist.con_defs "LCons(a,l) : llist(A)";
   44.20 +val LConsE = llist.mk_cases "LCons(a,l) : llist(A)";
   44.21  
   44.22  (*Proving freeness results*)
   44.23  val LCons_iff      = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
    45.1 --- a/src/ZF/ex/ListN.ML	Tue Jan 19 11:16:39 1999 +0100
    45.2 +++ b/src/ZF/ex/ListN.ML	Tue Jan 19 11:18:11 1999 +0100
    45.3 @@ -9,8 +9,6 @@
    45.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    45.5  *)
    45.6  
    45.7 -open ListN;
    45.8 -
    45.9  Goal "l:list(A) ==> <length(l),l> : listn(A)";
   45.10  by (etac list.induct 1);
   45.11  by (ALLGOALS Asm_simp_tac);
   45.12 @@ -40,8 +38,8 @@
   45.13  by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs)));
   45.14  qed "listn_append";
   45.15  
   45.16 -val Nil_listn_case = listn.mk_cases list.con_defs "<i,Nil> : listn(A)"
   45.17 -and Cons_listn_case = listn.mk_cases list.con_defs "<i,Cons(x,l)> : listn(A)";
   45.18 +val Nil_listn_case  = listn.mk_cases "<i,Nil> : listn(A)"
   45.19 +and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> : listn(A)";
   45.20  
   45.21 -val zero_listn_case = listn.mk_cases list.con_defs "<0,l> : listn(A)"
   45.22 -and succ_listn_case = listn.mk_cases list.con_defs "<succ(i),l> : listn(A)";
   45.23 +val zero_listn_case = listn.mk_cases "<0,l> : listn(A)"
   45.24 +and succ_listn_case = listn.mk_cases "<succ(i),l> : listn(A)";
    46.1 --- a/src/ZF/ex/PropLog.ML	Tue Jan 19 11:16:39 1999 +0100
    46.2 +++ b/src/ZF/ex/PropLog.ML	Tue Jan 19 11:18:11 1999 +0100
    46.3 @@ -40,7 +40,7 @@
    46.4  
    46.5  val thms_in_pl = thms.dom_subset RS subsetD;
    46.6  
    46.7 -val ImpE = prop.mk_cases prop.con_defs "p=>q : prop";
    46.8 +val ImpE = prop.mk_cases "p=>q : prop";
    46.9  
   46.10  (*Stronger Modus Ponens rule: no typechecking!*)
   46.11  Goal "[| H |- p=>q;  H |- p |] ==> H |- q";
   46.12 @@ -166,22 +166,14 @@
   46.13    we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
   46.14  Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
   46.15  by (etac prop.induct 1);
   46.16 -by (Simp_tac 1);
   46.17 -by (Asm_simp_tac 1);
   46.18 -by (fast_tac (claset() addSEs prop.free_SEs) 1);
   46.19 -by (Asm_simp_tac 1);
   46.20 -by (Fast_tac 1);
   46.21 +by Auto_tac;
   46.22  qed "hyps_Diff";
   46.23  
   46.24  (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
   46.25    we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
   46.26  Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
   46.27  by (etac prop.induct 1);
   46.28 -by (Simp_tac 1);
   46.29 -by (Asm_simp_tac 1);
   46.30 -by (fast_tac (claset() addSEs prop.free_SEs) 1);
   46.31 -by (Asm_simp_tac 1);
   46.32 -by (Fast_tac 1);
   46.33 +by Auto_tac;
   46.34  qed "hyps_cons";
   46.35  
   46.36  (** Two lemmas for use with weaken_left **)
    47.1 --- a/src/ZF/ex/Rmap.ML	Tue Jan 19 11:16:39 1999 +0100
    47.2 +++ b/src/ZF/ex/Rmap.ML	Tue Jan 19 11:18:11 1999 +0100
    47.3 @@ -6,8 +6,6 @@
    47.4  Inductive definition of an operator to "map" a relation over a list
    47.5  *)
    47.6  
    47.7 -open Rmap;
    47.8 -
    47.9  Goalw rmap.defs "r<=s ==> rmap(r) <= rmap(s)";
   47.10  by (rtac lfp_mono 1);
   47.11  by (REPEAT (rtac rmap.bnd_mono 1));
   47.12 @@ -15,8 +13,8 @@
   47.13                        basic_monos) 1));
   47.14  qed "rmap_mono";
   47.15  
   47.16 -val Nil_rmap_case = rmap.mk_cases list.con_defs "<Nil,zs> : rmap(r)"
   47.17 -and Cons_rmap_case = rmap.mk_cases list.con_defs "<Cons(x,xs),zs> : rmap(r)";
   47.18 +val Nil_rmap_case  = rmap.mk_cases "<Nil,zs> : rmap(r)"
   47.19 +and Cons_rmap_case = rmap.mk_cases "<Cons(x,xs),zs> : rmap(r)";
   47.20  
   47.21  AddIs  rmap.intrs;
   47.22  AddSEs [Nil_rmap_case, Cons_rmap_case];
   47.23 @@ -43,16 +41,16 @@
   47.24  (** If f is a function then rmap(f) behaves as expected. **)
   47.25  
   47.26  Goal "f: A->B ==> rmap(f): list(A)->list(B)";
   47.27 -by (asm_full_simp_tac 
   47.28 -    (simpset() addsimps [Pi_iff, rmap_rel_type, rmap_functional, rmap_total]) 1);
   47.29 +by (asm_full_simp_tac (simpset() addsimps [Pi_iff, rmap_rel_type,
   47.30 +					   rmap_functional, rmap_total]) 1);
   47.31  qed "rmap_fun_type";
   47.32  
   47.33  Goalw [apply_def] "rmap(f)`Nil = Nil";
   47.34  by (Blast_tac 1);
   47.35  qed "rmap_Nil";
   47.36  
   47.37 -Goal "[| f: A->B;  x: A;  xs: list(A) |] ==> \
   47.38 -\                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
   47.39 +Goal "[| f: A->B;  x: A;  xs: list(A) |]  \
   47.40 +\     ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
   47.41  by (rtac apply_equality 1);
   47.42  by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
   47.43  qed "rmap_Cons";