removal of the (thm list) argument of mk_cases

--- a/NEWS	Tue Jan 19 11:16:39 1999 +0100
+++ b/NEWS	Tue Jan 19 11:18:11 1999 +0100
@@ -11,6 +11,10 @@
 * ZF: The con_defs part of an inductive definition may no longer refer to 
   constants declared in the same theory;
 
+* HOL, ZF: the function mk_cases, generated by the inductive definition 
+  package, has lost an argument.  To simplify its result, it uses the default
+  simpset instead of a supplied list of theorems.
+
 
 *** Proof tools ***
 
@@ -68,6 +72,9 @@
 
 * the datatype declaration of type T now defines the recursor T_rec;
 
+* simplification automatically does freeness reasoning for datatype
+  constructors;
+
 * The syntax "if P then x else y" is now available in addition to if(P,x,y).
 
 

--- a/doc-src/Inductive/ind-defs.tex	Tue Jan 19 11:16:39 1999 +0100
+++ b/doc-src/Inductive/ind-defs.tex	Tue Jan 19 11:18:11 1999 +0100
@@ -632,9 +632,9 @@
 deduces the corresponding form of~$i$;  this is called rule inversion.  
 Here is a sample session: 
 \begin{ttbox}
-listn.mk_cases list.con_defs "<i,Nil> : listn(A)";
+listn.mk_cases "<i,Nil> : listn(A)";
 {\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm}
-listn.mk_cases list.con_defs "<i,Cons(a,l)> : listn(A)";
+listn.mk_cases "<i,Cons(a,l)> : listn(A)";
 {\out "[| <?i, Cons(?a, ?l)> : listn(?A);}
 {\out     !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q }
 {\out  |] ==> ?Q" : thm}

--- a/doc-src/Logics/HOL.tex	Tue Jan 19 11:16:39 1999 +0100
+++ b/doc-src/Logics/HOL.tex	Tue Jan 19 11:18:11 1999 +0100
@@ -2657,7 +2657,7 @@
 \item[\tt elim] is the head of the list \texttt{elims}.
   
 \item[\tt mk_cases] is a function to create simplified instances of {\tt
-elim}, using freeness reasoning on some underlying datatype.
+elim} using freeness reasoning on underlying datatypes.
 \end{description}
 
 For an inductive definition, the result structure contains the
@@ -2676,7 +2676,7 @@
 val intrs        : thm list
 val elims        : thm list
 val elim         : thm
-val mk_cases     : thm list -> string -> thm
+val mk_cases     : string -> thm
 {\it(Inductive definitions only)} 
 val induct       : thm
 {\it(coinductive definitions only)}

--- a/doc-src/Logics/logics.ind	Tue Jan 19 11:16:39 1999 +0100
+++ b/doc-src/Logics/logics.ind	Tue Jan 19 11:18:11 1999 +0100
@@ -1,652 +1,659 @@
 \begin{theindex}
 
-  \item {\tt !} symbol, 2, 4, 11, 12, 24
-  \item {\tt[]} symbol, 24
-  \item {\tt\#} symbol, 24
-  \item {\tt\#*} symbol, 80
-  \item {\tt\#+} symbol, 80
-  \item {\tt\&} symbol, 2, 56
-  \item {\tt *} symbol, 3, 21, 71
-  \item {\tt *} type, 19
-  \item {\tt +} symbol, 3, 21, 71
-  \item {\tt +} type, 19
-  \item {\tt -} symbol, 3, 21, 80
-  \item {\tt -->} symbol, 2, 56, 71
-  \item {\tt :} symbol, 10
-  \item {\tt <} constant, 22
-  \item {\tt <} symbol, 21
-  \item {\tt <->} symbol, 56
-  \item {\tt <=} constant, 22
-  \item {\tt <=} symbol, 10
-  \item {\tt =} symbol, 2, 56, 71
-  \item {\tt ?} symbol, 2, 4, 11, 12
-  \item {\tt ?!} symbol, 2
-  \item {\tt\at} symbol, 2, 24
-  \item {\tt `} symbol, 71
-  \item {\tt ``} symbol, 10
-  \item \verb'{}' symbol, 10
-  \item {\tt |} symbol, 2, 56
-  \item {\tt |-|} symbol, 80
+  \item {\tt !} symbol, 6, 8, 15, 16, 28
+  \item {\tt[]} symbol, 28
+  \item {\tt\#} symbol, 28
+  \item {\tt\#*} symbol, 83
+  \item {\tt\#+} symbol, 83
+  \item {\tt\&} symbol, 6, 59
+  \item {\tt *} symbol, 7, 25, 74
+  \item {\tt *} type, 23
+  \item {\tt +} symbol, 7, 25, 74
+  \item {\tt +} type, 23
+  \item {\tt -} symbol, 7, 25, 83
+  \item {\tt -->} symbol, 6, 59, 74
+  \item {\tt :} symbol, 14
+  \item {\tt <} constant, 26
+  \item {\tt <} symbol, 25
+  \item {\tt <->} symbol, 59
+  \item {\tt <=} constant, 26
+  \item {\tt <=} symbol, 14
+  \item {\tt =} symbol, 6, 59, 74
+  \item {\tt ?} symbol, 6, 8, 15, 16
+  \item {\tt ?!} symbol, 6
+  \item {\tt\at} symbol, 6, 28
+  \item {\tt `} symbol, 74
+  \item {\tt ``} symbol, 14
+  \item \verb'{}' symbol, 14
+  \item {\tt |} symbol, 6, 59
+  \item {\tt |-|} symbol, 83
 
   \indexspace
 
-  \item {\tt 0} constant, 21, 69
+  \item {\tt 0} constant, 25, 72
 
   \indexspace
 
-  \item {\tt absdiff_def} theorem, 80
-  \item {\tt add_assoc} theorem, 80
-  \item {\tt add_commute} theorem, 80
-  \item {\tt add_def} theorem, 80
-  \item {\tt add_inverse_diff} theorem, 80
-  \item {\tt add_mp_tac}, \bold{78}
-  \item {\tt add_mult_dist} theorem, 80
-  \item {\tt add_safes}, \bold{62}
-  \item {\tt add_typing} theorem, 80
-  \item {\tt add_unsafes}, \bold{62}
-  \item {\tt addC0} theorem, 80
-  \item {\tt addC_succ} theorem, 80
-  \item {\tt Addsplits}, \bold{18}
-  \item {\tt addsplits}, \bold{18}, 23, 35
-  \item {\tt ALL} symbol, 2, 4, 11, 12, 56
-  \item {\tt All} constant, 2, 56
-  \item {\tt All_def} theorem, 6
-  \item {\tt all_dupE} theorem, 8
-  \item {\tt allE} theorem, 8
-  \item {\tt allI} theorem, 8
-  \item {\tt allL} theorem, 58, 62
-  \item {\tt allL_thin} theorem, 59
-  \item {\tt allR} theorem, 58
-  \item {\tt and_def} theorem, 6
-  \item {\tt arg_cong} theorem, 7
-  \item {\tt Arith} theory, 22, 79
+  \item {\tt absdiff_def} theorem, 83
+  \item {\tt add_assoc} theorem, 83
+  \item {\tt add_commute} theorem, 83
+  \item {\tt add_def} theorem, 83
+  \item {\tt add_inverse_diff} theorem, 83
+  \item {\tt add_mp_tac}, \bold{81}
+  \item {\tt add_mult_dist} theorem, 83
+  \item {\tt add_safes}, \bold{65}
+  \item {\tt add_typing} theorem, 83
+  \item {\tt add_unsafes}, \bold{65}
+  \item {\tt addC0} theorem, 83
+  \item {\tt addC_succ} theorem, 83
+  \item {\tt Addsplits}, \bold{22}
+  \item {\tt addsplits}, \bold{22}, 27, 39
+  \item {\tt ALL} symbol, 6, 8, 15, 16, 59
+  \item {\tt All} constant, 6, 59
+  \item {\tt All_def} theorem, 10
+  \item {\tt all_dupE} theorem, 12
+  \item {\tt allE} theorem, 12
+  \item {\tt allI} theorem, 12
+  \item {\tt allL} theorem, 61, 65
+  \item {\tt allL_thin} theorem, 62
+  \item {\tt allR} theorem, 61
+  \item {\tt and_def} theorem, 10
+  \item {\tt arg_cong} theorem, 11
+  \item {\tt Arith} theory, 26, 82
   \item assumptions
-    \subitem in {\CTT}, 68, 78
+    \subitem in {\CTT}, 71, 81
 
   \indexspace
 
-  \item {\tt Ball} constant, 10, 12
-  \item {\tt Ball_def} theorem, 13
-  \item {\tt ballE} theorem, 14
-  \item {\tt ballI} theorem, 14
-  \item {\tt basic} theorem, 58
-  \item {\tt basic_defs}, \bold{76}
-  \item {\tt best_tac}, \bold{63}
-  \item {\tt Bex} constant, 10, 12
-  \item {\tt Bex_def} theorem, 13
-  \item {\tt bexCI} theorem, 12, 14
-  \item {\tt bexE} theorem, 14
-  \item {\tt bexI} theorem, 12, 14
-  \item {\textit {bool}} type, 3
-  \item {\tt box_equals} theorem, 7, 9
-  \item {\tt bspec} theorem, 14
-  \item {\tt butlast} constant, 24
+  \item {\tt Ball} constant, 14, 16
+  \item {\tt Ball_def} theorem, 17
+  \item {\tt ballE} theorem, 18
+  \item {\tt ballI} theorem, 18
+  \item {\tt basic} theorem, 61
+  \item {\tt basic_defs}, \bold{79}
+  \item {\tt best_tac}, \bold{66}
+  \item {\tt Bex} constant, 14, 16
+  \item {\tt Bex_def} theorem, 17
+  \item {\tt bexCI} theorem, 16, 18
+  \item {\tt bexE} theorem, 18
+  \item {\tt bexI} theorem, 16, 18
+  \item {\textit {bool}} type, 7
+  \item {\tt box_equals} theorem, 11, 13
+  \item {\tt bspec} theorem, 18
+  \item {\tt butlast} constant, 28
 
   \indexspace
 
-  \item {\tt case} symbol, 5, 22, 23, 35
-  \item {\tt case_tac}, \bold{9}
-  \item {\tt ccontr} theorem, 8
-  \item {\tt classical} theorem, 8
-  \item {\tt coinductive}, 47--50
-  \item {\tt Collect} constant, 10, 12
-  \item {\tt Collect_mem_eq} theorem, 12, 13
-  \item {\tt CollectD} theorem, 14, 53
-  \item {\tt CollectE} theorem, 14
-  \item {\tt CollectI} theorem, 14, 53
-  \item {\tt comp_rls}, \bold{76}
-  \item {\tt Compl} constant, 10
-  \item {\tt Compl_def} theorem, 13
-  \item {\tt Compl_disjoint} theorem, 16
-  \item {\tt Compl_Int} theorem, 16
-  \item {\tt Compl_partition} theorem, 16
-  \item {\tt Compl_Un} theorem, 16
-  \item {\tt ComplD} theorem, 15
-  \item {\tt ComplI} theorem, 15
-  \item {\tt concat} constant, 24
-  \item {\tt cong} theorem, 7
-  \item {\tt conj_cong}, 17
-  \item {\tt conjE} theorem, 7
-  \item {\tt conjI} theorem, 7
-  \item {\tt conjL} theorem, 58
-  \item {\tt conjR} theorem, 58
-  \item {\tt conjunct1} theorem, 7
-  \item {\tt conjunct2} theorem, 7
-  \item {\tt conL} theorem, 59
-  \item {\tt conR} theorem, 59
-  \item Constructive Type Theory, 68--90
-  \item {\tt contr} constant, 69
-  \item {\tt could_res}, \bold{61}
-  \item {\tt could_resolve_seq}, \bold{61}
-  \item {\tt CTT} theory, 68
-  \item {\tt cut} theorem, 58
-  \item {\tt cutL_tac}, \bold{60}
-  \item {\tt cutR_tac}, \bold{60}
+  \item {\tt case} symbol, 9, 26, 27, 39
+  \item {\tt case_tac}, \bold{13}
+  \item {\tt CCL} theory, 1
+  \item {\tt ccontr} theorem, 12
+  \item {\tt classical} theorem, 12
+  \item {\tt coinductive}, 51--53
+  \item {\tt Collect} constant, 14, 16
+  \item {\tt Collect_mem_eq} theorem, 16, 17
+  \item {\tt CollectD} theorem, 18, 56
+  \item {\tt CollectE} theorem, 18
+  \item {\tt CollectI} theorem, 18, 57
+  \item {\tt comp_rls}, \bold{79}
+  \item {\tt Compl} constant, 14
+  \item {\tt Compl_def} theorem, 17
+  \item {\tt Compl_disjoint} theorem, 20
+  \item {\tt Compl_Int} theorem, 20
+  \item {\tt Compl_partition} theorem, 20
+  \item {\tt Compl_Un} theorem, 20
+  \item {\tt ComplD} theorem, 19
+  \item {\tt ComplI} theorem, 19
+  \item {\tt concat} constant, 28
+  \item {\tt cong} theorem, 11
+  \item {\tt conj_cong}, 21
+  \item {\tt conjE} theorem, 11
+  \item {\tt conjI} theorem, 11
+  \item {\tt conjL} theorem, 61
+  \item {\tt conjR} theorem, 61
+  \item {\tt conjunct1} theorem, 11
+  \item {\tt conjunct2} theorem, 11
+  \item {\tt conL} theorem, 62
+  \item {\tt conR} theorem, 62
+  \item Constructive Type Theory, 71--93
+  \item {\tt contr} constant, 72
+  \item {\tt could_res}, \bold{64}
+  \item {\tt could_resolve_seq}, \bold{64}
+  \item {\tt CTT} theory, 1, 71
+  \item {\tt Cube} theory, 1
+  \item {\tt cut} theorem, 61
+  \item {\tt cutL_tac}, \bold{63}
+  \item {\tt cutR_tac}, \bold{63}
 
   \indexspace
 
-  \item {\tt datatype}, 32--40
-  \item {\tt Delsplits}, \bold{18}
-  \item {\tt delsplits}, \bold{18}
-  \item {\tt diff_0_eq_0} theorem, 80
-  \item {\tt diff_def} theorem, 80
-  \item {\tt diff_self_eq_0} theorem, 80
-  \item {\tt diff_succ_succ} theorem, 80
-  \item {\tt diff_typing} theorem, 80
-  \item {\tt diffC0} theorem, 80
-  \item {\tt disjCI} theorem, 8
-  \item {\tt disjE} theorem, 7
-  \item {\tt disjI1} theorem, 7
-  \item {\tt disjI2} theorem, 7
-  \item {\tt disjL} theorem, 58
-  \item {\tt disjR} theorem, 58
-  \item {\tt div} symbol, 21, 80
-  \item {\tt div_def} theorem, 80
-  \item {\tt div_geq} theorem, 22
-  \item {\tt div_less} theorem, 22
-  \item {\tt Divides} theory, 22
-  \item {\tt double_complement} theorem, 16
-  \item {\tt drop} constant, 24
-  \item {\tt dropWhile} constant, 24
+  \item {\tt datatype}, 36--44
+  \item {\tt Delsplits}, \bold{22}
+  \item {\tt delsplits}, \bold{22}
+  \item {\tt diff_0_eq_0} theorem, 83
+  \item {\tt diff_def} theorem, 83
+  \item {\tt diff_self_eq_0} theorem, 83
+  \item {\tt diff_succ_succ} theorem, 83
+  \item {\tt diff_typing} theorem, 83
+  \item {\tt diffC0} theorem, 83
+  \item {\tt disjCI} theorem, 12
+  \item {\tt disjE} theorem, 11
+  \item {\tt disjI1} theorem, 11
+  \item {\tt disjI2} theorem, 11
+  \item {\tt disjL} theorem, 61
+  \item {\tt disjR} theorem, 61
+  \item {\tt div} symbol, 25, 83
+  \item {\tt div_def} theorem, 83
+  \item {\tt div_geq} theorem, 26
+  \item {\tt div_less} theorem, 26
+  \item {\tt Divides} theory, 26
+  \item {\tt double_complement} theorem, 20
+  \item {\tt drop} constant, 28
+  \item {\tt dropWhile} constant, 28
 
   \indexspace
 
-  \item {\tt Elem} constant, 69
-  \item {\tt elim_rls}, \bold{76}
-  \item {\tt elimL_rls}, \bold{76}
-  \item {\tt empty_def} theorem, 13
-  \item {\tt empty_pack}, \bold{62}
-  \item {\tt emptyE} theorem, 15
-  \item {\tt Eps} constant, 2, 4
-  \item {\tt Eq} constant, 69
-  \item {\tt eq} constant, 69, 74
-  \item {\tt EqC} theorem, 75
-  \item {\tt EqE} theorem, 75
-  \item {\tt Eqelem} constant, 69
-  \item {\tt EqF} theorem, 75
-  \item {\tt EqFL} theorem, 75
-  \item {\tt EqI} theorem, 75
-  \item {\tt Eqtype} constant, 69
-  \item {\tt equal_tac}, \bold{77}
-  \item {\tt equal_types} theorem, 72
-  \item {\tt equal_typesL} theorem, 72
-  \item {\tt equalityCE} theorem, 12, 14, 53, 54
-  \item {\tt equalityD1} theorem, 14
-  \item {\tt equalityD2} theorem, 14
-  \item {\tt equalityE} theorem, 14
-  \item {\tt equalityI} theorem, 14
-  \item {\tt EX} symbol, 2, 4, 11, 12, 56
-  \item {\tt Ex} constant, 2, 56
-  \item {\tt EX!} symbol, 2
-  \item {\tt Ex1} constant, 2
-  \item {\tt Ex1_def} theorem, 6
-  \item {\tt ex1E} theorem, 8
-  \item {\tt ex1I} theorem, 8
-  \item {\tt Ex_def} theorem, 6
-  \item {\tt exCI} theorem, 8
-  \item {\tt excluded_middle} theorem, 8
-  \item {\tt exE} theorem, 8
-  \item {\tt exhaust_tac}, \bold{36}
-  \item {\tt exI} theorem, 8
-  \item {\tt exL} theorem, 58
-  \item {\tt Exp} theory, 51
-  \item {\tt exR} theorem, 58, 62, 64
-  \item {\tt exR_thin} theorem, 59, 64, 65
-  \item {\tt ext} theorem, 5, 6
+  \item {\tt Elem} constant, 72
+  \item {\tt elim_rls}, \bold{79}
+  \item {\tt elimL_rls}, \bold{79}
+  \item {\tt empty_def} theorem, 17
+  \item {\tt empty_pack}, \bold{65}
+  \item {\tt emptyE} theorem, 19
+  \item {\tt Eps} constant, 6, 8
+  \item {\tt Eq} constant, 72
+  \item {\tt eq} constant, 72, 77
+  \item {\tt EqC} theorem, 78
+  \item {\tt EqE} theorem, 78
+  \item {\tt Eqelem} constant, 72
+  \item {\tt EqF} theorem, 78
+  \item {\tt EqFL} theorem, 78
+  \item {\tt EqI} theorem, 78
+  \item {\tt Eqtype} constant, 72
+  \item {\tt equal_tac}, \bold{80}
+  \item {\tt equal_types} theorem, 75
+  \item {\tt equal_typesL} theorem, 75
+  \item {\tt equalityCE} theorem, 16, 18, 56, 57
+  \item {\tt equalityD1} theorem, 18
+  \item {\tt equalityD2} theorem, 18
+  \item {\tt equalityE} theorem, 18
+  \item {\tt equalityI} theorem, 18
+  \item {\tt EX} symbol, 6, 8, 15, 16, 59
+  \item {\tt Ex} constant, 6, 59
+  \item {\tt EX!} symbol, 6
+  \item {\tt Ex1} constant, 6
+  \item {\tt Ex1_def} theorem, 10
+  \item {\tt ex1E} theorem, 12
+  \item {\tt ex1I} theorem, 12
+  \item {\tt Ex_def} theorem, 10
+  \item {\tt exCI} theorem, 12
+  \item {\tt excluded_middle} theorem, 12
+  \item {\tt exE} theorem, 12
+  \item {\tt exhaust_tac}, \bold{40}
+  \item {\tt exI} theorem, 12
+  \item {\tt exL} theorem, 61
+  \item {\tt Exp} theory, 55
+  \item {\tt exR} theorem, 61, 65, 67
+  \item {\tt exR_thin} theorem, 62, 67, 68
+  \item {\tt ext} theorem, 9, 10
 
   \indexspace
 
-  \item {\tt F} constant, 69
-  \item {\tt False} constant, 2, 56
-  \item {\tt False_def} theorem, 6
-  \item {\tt FalseE} theorem, 7
-  \item {\tt FalseL} theorem, 58
-  \item {\tt fast_tac}, \bold{63}
-  \item {\tt FE} theorem, 75, 79
-  \item {\tt FEL} theorem, 75
-  \item {\tt FF} theorem, 75
-  \item {\tt filseq_resolve_tac}, \bold{61}
-  \item {\tt filt_resolve_tac}, 61, 77
-  \item {\tt filter} constant, 24
-  \item flex-flex constraints, 57
-  \item {\tt FOL} theory, 78
-  \item {\tt foldl} constant, 24
-  \item {\tt form_rls}, \bold{76}
-  \item {\tt formL_rls}, \bold{76}
-  \item {\tt forms_of_seq}, \bold{60}
-  \item {\tt fst} constant, 19, 69, 74
-  \item {\tt fst_conv} theorem, 19
-  \item {\tt fst_def} theorem, 74
-  \item {\tt Fun} theory, 17
-  \item {\textit {fun}} type, 3
-  \item {\tt fun_cong} theorem, 7
+  \item {\tt F} constant, 72
+  \item {\tt False} constant, 6, 59
+  \item {\tt False_def} theorem, 10
+  \item {\tt FalseE} theorem, 11
+  \item {\tt FalseL} theorem, 61
+  \item {\tt fast_tac}, \bold{66}
+  \item {\tt FE} theorem, 78, 82
+  \item {\tt FEL} theorem, 78
+  \item {\tt FF} theorem, 78
+  \item {\tt filseq_resolve_tac}, \bold{64}
+  \item {\tt filt_resolve_tac}, 64, 80
+  \item {\tt filter} constant, 28
+  \item flex-flex constraints, 60
+  \item {\tt FOL} theory, 81
+  \item {\tt foldl} constant, 28
+  \item {\tt form_rls}, \bold{79}
+  \item {\tt formL_rls}, \bold{79}
+  \item {\tt forms_of_seq}, \bold{63}
+  \item {\tt fst} constant, 23, 72, 77
+  \item {\tt fst_conv} theorem, 23
+  \item {\tt fst_def} theorem, 77
+  \item {\tt Fun} theory, 21
+  \item {\textit {fun}} type, 7
+  \item {\tt fun_cong} theorem, 11
   \item function applications
-    \subitem in \CTT, 71
+    \subitem in \CTT, 74
 
   \indexspace
 
-  \item {\tt hd} constant, 24
-  \item higher-order logic, 1--54
-  \item {\tt HOL} theory, 1
-  \item {\sc hol} system, 1, 4
-  \item {\tt HOL_basic_ss}, \bold{17}
-  \item {\tt HOL_cs}, \bold{18}
-  \item {\tt HOL_quantifiers}, \bold{4}, 12
-  \item {\tt HOL_ss}, \bold{17}
-  \item {\tt hyp_rew_tac}, \bold{78}
-  \item {\tt hyp_subst_tac}, 17
+  \item {\tt hd} constant, 28
+  \item higher-order logic, 5--57
+  \item {\tt HOL} theory, 1, 5
+  \item {\sc hol} system, 5, 8
+  \item {\tt HOL_basic_ss}, \bold{21}
+  \item {\tt HOL_cs}, \bold{22}
+  \item {\tt HOL_quantifiers}, \bold{8}, 16
+  \item {\tt HOL_ss}, \bold{21}
+  \item {\tt HOLCF} theory, 1
+  \item {\tt hyp_rew_tac}, \bold{81}
+  \item {\tt hyp_subst_tac}, 21
 
   \indexspace
 
-  \item {\textit {i}} type, 68
-  \item {\tt If} constant, 2
-  \item {\tt if_def} theorem, 6
-  \item {\tt if_not_P} theorem, 8
-  \item {\tt if_P} theorem, 8
-  \item {\tt iff} theorem, 5, 6
-  \item {\tt iff_def} theorem, 58
-  \item {\tt iffCE} theorem, 8, 12
-  \item {\tt iffD1} theorem, 7
-  \item {\tt iffD2} theorem, 7
-  \item {\tt iffE} theorem, 7
-  \item {\tt iffI} theorem, 7
-  \item {\tt iffL} theorem, 59, 66
-  \item {\tt iffR} theorem, 59
-  \item {\tt image_def} theorem, 13
-  \item {\tt imageE} theorem, 15
-  \item {\tt imageI} theorem, 15
-  \item {\tt impCE} theorem, 8
-  \item {\tt impE} theorem, 7
-  \item {\tt impI} theorem, 5
-  \item {\tt impL} theorem, 58
-  \item {\tt impR} theorem, 58
-  \item {\tt in} symbol, 3
-  \item {\textit {ind}} type, 20
-  \item {\tt induct_tac}, 22, \bold{36}
-  \item {\tt inductive}, 47--50
-  \item {\tt inj} constant, 17
-  \item {\tt inj_def} theorem, 17
-  \item {\tt inj_Inl} theorem, 21
-  \item {\tt inj_Inr} theorem, 21
-  \item {\tt inj_on} constant, 17
-  \item {\tt inj_on_def} theorem, 17
-  \item {\tt inj_Suc} theorem, 21
-  \item {\tt Inl} constant, 21
-  \item {\tt inl} constant, 69, 74, 84
-  \item {\tt Inl_not_Inr} theorem, 21
-  \item {\tt Inr} constant, 21
-  \item {\tt inr} constant, 69, 74
-  \item {\tt insert} constant, 10
-  \item {\tt insert_def} theorem, 13
-  \item {\tt insertE} theorem, 15
-  \item {\tt insertI1} theorem, 15
-  \item {\tt insertI2} theorem, 15
-  \item {\tt INT} symbol, 10--12
-  \item {\tt Int} symbol, 10
-  \item {\tt Int_absorb} theorem, 16
-  \item {\tt Int_assoc} theorem, 16
-  \item {\tt Int_commute} theorem, 16
-  \item {\tt INT_D} theorem, 15
-  \item {\tt Int_def} theorem, 13
-  \item {\tt INT_E} theorem, 15
-  \item {\tt Int_greatest} theorem, 16
-  \item {\tt INT_I} theorem, 15
-  \item {\tt Int_Inter_image} theorem, 16
-  \item {\tt Int_lower1} theorem, 16
-  \item {\tt Int_lower2} theorem, 16
-  \item {\tt Int_Un_distrib} theorem, 16
-  \item {\tt Int_Union} theorem, 16
-  \item {\tt IntD1} theorem, 15
-  \item {\tt IntD2} theorem, 15
-  \item {\tt IntE} theorem, 15
-  \item {\tt INTER} constant, 10
-  \item {\tt Inter} constant, 10
-  \item {\tt INTER1} constant, 10
-  \item {\tt INTER1_def} theorem, 13
-  \item {\tt INTER_def} theorem, 13
-  \item {\tt Inter_def} theorem, 13
-  \item {\tt Inter_greatest} theorem, 16
-  \item {\tt Inter_lower} theorem, 16
-  \item {\tt Inter_Un_distrib} theorem, 16
-  \item {\tt InterD} theorem, 15
-  \item {\tt InterE} theorem, 15
-  \item {\tt InterI} theorem, 15
-  \item {\tt IntI} theorem, 15
-  \item {\tt intr_rls}, \bold{76}
-  \item {\tt intr_tac}, \bold{77}, 86, 87
-  \item {\tt intrL_rls}, \bold{76}
-  \item {\tt inv} constant, 17
-  \item {\tt inv_def} theorem, 17
+  \item {\textit {i}} type, 71
+  \item {\tt If} constant, 6
+  \item {\tt if_def} theorem, 10
+  \item {\tt if_not_P} theorem, 12
+  \item {\tt if_P} theorem, 12
+  \item {\tt iff} theorem, 9, 10
+  \item {\tt iff_def} theorem, 61
+  \item {\tt iffCE} theorem, 12, 16
+  \item {\tt iffD1} theorem, 11
+  \item {\tt iffD2} theorem, 11
+  \item {\tt iffE} theorem, 11
+  \item {\tt iffI} theorem, 11
+  \item {\tt iffL} theorem, 62, 69
+  \item {\tt iffR} theorem, 62
+  \item {\tt ILL} theory, 1
+  \item {\tt image_def} theorem, 17
+  \item {\tt imageE} theorem, 19
+  \item {\tt imageI} theorem, 19
+  \item {\tt impCE} theorem, 12
+  \item {\tt impE} theorem, 11
+  \item {\tt impI} theorem, 9
+  \item {\tt impL} theorem, 61
+  \item {\tt impR} theorem, 61
+  \item {\tt in} symbol, 7
+  \item {\textit {ind}} type, 24
+  \item {\tt induct_tac}, 26, \bold{40}
+  \item {\tt inductive}, 51--53
+  \item {\tt inj} constant, 21
+  \item {\tt inj_def} theorem, 21
+  \item {\tt inj_Inl} theorem, 25
+  \item {\tt inj_Inr} theorem, 25
+  \item {\tt inj_on} constant, 21
+  \item {\tt inj_on_def} theorem, 21
+  \item {\tt inj_Suc} theorem, 25
+  \item {\tt Inl} constant, 25
+  \item {\tt inl} constant, 72, 77, 87
+  \item {\tt Inl_not_Inr} theorem, 25
+  \item {\tt Inr} constant, 25
+  \item {\tt inr} constant, 72, 77
+  \item {\tt insert} constant, 14
+  \item {\tt insert_def} theorem, 17
+  \item {\tt insertE} theorem, 19
+  \item {\tt insertI1} theorem, 19
+  \item {\tt insertI2} theorem, 19
+  \item {\tt INT} symbol, 14--16
+  \item {\tt Int} symbol, 14
+  \item {\tt Int_absorb} theorem, 20
+  \item {\tt Int_assoc} theorem, 20
+  \item {\tt Int_commute} theorem, 20
+  \item {\tt INT_D} theorem, 19
+  \item {\tt Int_def} theorem, 17
+  \item {\tt INT_E} theorem, 19
+  \item {\tt Int_greatest} theorem, 20
+  \item {\tt INT_I} theorem, 19
+  \item {\tt Int_Inter_image} theorem, 20
+  \item {\tt Int_lower1} theorem, 20
+  \item {\tt Int_lower2} theorem, 20
+  \item {\tt Int_Un_distrib} theorem, 20
+  \item {\tt Int_Union} theorem, 20
+  \item {\tt IntD1} theorem, 19
+  \item {\tt IntD2} theorem, 19
+  \item {\tt IntE} theorem, 19
+  \item {\tt INTER} constant, 14
+  \item {\tt Inter} constant, 14
+  \item {\tt INTER1} constant, 14
+  \item {\tt INTER1_def} theorem, 17
+  \item {\tt INTER_def} theorem, 17
+  \item {\tt Inter_def} theorem, 17
+  \item {\tt Inter_greatest} theorem, 20
+  \item {\tt Inter_lower} theorem, 20
+  \item {\tt Inter_Un_distrib} theorem, 20
+  \item {\tt InterD} theorem, 19
+  \item {\tt InterE} theorem, 19
+  \item {\tt InterI} theorem, 19
+  \item {\tt IntI} theorem, 19
+  \item {\tt intr_rls}, \bold{79}
+  \item {\tt intr_tac}, \bold{80}, 89, 90
+  \item {\tt intrL_rls}, \bold{79}
+  \item {\tt inv} constant, 21
+  \item {\tt inv_def} theorem, 21
 
   \indexspace
 
-  \item {\tt lam} symbol, 71
-  \item {\tt lambda} constant, 69, 71
+  \item {\tt lam} symbol, 74
+  \item {\tt lambda} constant, 72, 74
   \item $\lambda$-abstractions
-    \subitem in \CTT, 71
-  \item {\tt last} constant, 24
-  \item {\tt LEAST} constant, 3, 4, 22
-  \item {\tt Least} constant, 2
-  \item {\tt Least_def} theorem, 6
-  \item {\tt length} constant, 24
-  \item {\tt less_induct} theorem, 23
-  \item {\tt Let} constant, 2, 5
-  \item {\tt let} symbol, 3, 5
-  \item {\tt Let_def} theorem, 5, 6
-  \item {\tt LFilter} theory, 51
-  \item {\tt List} theory, 23, 24
-  \item {\textit{list}} type, 23
-  \item {\tt LK} theory, 55, 59
-  \item {\tt LK_dup_pack}, \bold{62}, 63
-  \item {\tt LK_pack}, \bold{62}
-  \item {\tt LList} theory, 51
+    \subitem in \CTT, 74
+  \item {\tt last} constant, 28
+  \item {\tt LCF} theory, 1
+  \item {\tt LEAST} constant, 7, 8, 26
+  \item {\tt Least} constant, 6
+  \item {\tt Least_def} theorem, 10
+  \item {\tt length} constant, 28
+  \item {\tt less_induct} theorem, 27
+  \item {\tt Let} constant, 6, 9
+  \item {\tt let} symbol, 7, 9
+  \item {\tt Let_def} theorem, 9, 10
+  \item {\tt LFilter} theory, 55
+  \item {\tt List} theory, 27, 28
+  \item {\textit{list}} type, 27
+  \item {\tt LK} theory, 1, 58, 62
+  \item {\tt LK_dup_pack}, \bold{65}, 66
+  \item {\tt LK_pack}, \bold{65}
+  \item {\tt LList} theory, 54
 
   \indexspace
 
-  \item {\tt map} constant, 24
-  \item {\tt max} constant, 3, 22
-  \item {\tt mem} symbol, 24
-  \item {\tt mem_Collect_eq} theorem, 12, 13
-  \item {\tt min} constant, 3, 22
-  \item {\tt minus} class, 3
-  \item {\tt mod} symbol, 21, 80
-  \item {\tt mod_def} theorem, 80
-  \item {\tt mod_geq} theorem, 22
-  \item {\tt mod_less} theorem, 22
-  \item {\tt mono} constant, 3
-  \item {\tt mp} theorem, 5
-  \item {\tt mp_tac}, \bold{78}
-  \item {\tt mult_assoc} theorem, 80
-  \item {\tt mult_commute} theorem, 80
-  \item {\tt mult_def} theorem, 80
-  \item {\tt mult_typing} theorem, 80
-  \item {\tt multC0} theorem, 80
-  \item {\tt multC_succ} theorem, 80
-  \item {\tt mutual_induct_tac}, \bold{36}
+  \item {\tt map} constant, 28
+  \item {\tt max} constant, 7, 26
+  \item {\tt mem} symbol, 28
+  \item {\tt mem_Collect_eq} theorem, 16, 17
+  \item {\tt min} constant, 7, 26
+  \item {\tt minus} class, 7
+  \item {\tt mod} symbol, 25, 83
+  \item {\tt mod_def} theorem, 83
+  \item {\tt mod_geq} theorem, 26
+  \item {\tt mod_less} theorem, 26
+  \item {\tt Modal} theory, 1
+  \item {\tt mono} constant, 7
+  \item {\tt mp} theorem, 9
+  \item {\tt mp_tac}, \bold{81}
+  \item {\tt mult_assoc} theorem, 83
+  \item {\tt mult_commute} theorem, 83
+  \item {\tt mult_def} theorem, 83
+  \item {\tt mult_typing} theorem, 83
+  \item {\tt multC0} theorem, 83
+  \item {\tt multC_succ} theorem, 83
+  \item {\tt mutual_induct_tac}, \bold{40}
 
   \indexspace
 
-  \item {\tt N} constant, 69
-  \item {\tt n_not_Suc_n} theorem, 21
-  \item {\tt Nat} theory, 22
-  \item {\textit {nat}} type, 21, 22
-  \item {\textit{nat}} type, 20--23
-  \item {\tt nat_induct} theorem, 21
-  \item {\tt nat_rec} constant, 22
-  \item {\tt NatDef} theory, 20
-  \item {\tt NC0} theorem, 73
-  \item {\tt NC_succ} theorem, 73
-  \item {\tt NE} theorem, 72, 73, 81
-  \item {\tt NEL} theorem, 73
-  \item {\tt NF} theorem, 73, 82
-  \item {\tt NI0} theorem, 73
-  \item {\tt NI_succ} theorem, 73
-  \item {\tt NI_succL} theorem, 73
-  \item {\tt NIO} theorem, 81
-  \item {\tt Not} constant, 2, 56
-  \item {\tt not_def} theorem, 6
-  \item {\tt not_sym} theorem, 7
-  \item {\tt notE} theorem, 7
-  \item {\tt notI} theorem, 7
-  \item {\tt notL} theorem, 58
-  \item {\tt notnotD} theorem, 8
-  \item {\tt notR} theorem, 58
-  \item {\tt null} constant, 24
+  \item {\tt N} constant, 72
+  \item {\tt n_not_Suc_n} theorem, 25
+  \item {\tt Nat} theory, 26
+  \item {\textit {nat}} type, 25, 26
+  \item {\textit{nat}} type, 24--27
+  \item {\tt nat_induct} theorem, 25
+  \item {\tt nat_rec} constant, 26
+  \item {\tt NatDef} theory, 24
+  \item {\tt NC0} theorem, 76
+  \item {\tt NC_succ} theorem, 76
+  \item {\tt NE} theorem, 75, 76, 84
+  \item {\tt NEL} theorem, 76
+  \item {\tt NF} theorem, 76, 85
+  \item {\tt NI0} theorem, 76
+  \item {\tt NI_succ} theorem, 76
+  \item {\tt NI_succL} theorem, 76
+  \item {\tt NIO} theorem, 84
+  \item {\tt Not} constant, 6, 59
+  \item {\tt not_def} theorem, 10
+  \item {\tt not_sym} theorem, 11
+  \item {\tt notE} theorem, 11
+  \item {\tt notI} theorem, 11
+  \item {\tt notL} theorem, 61
+  \item {\tt notnotD} theorem, 12
+  \item {\tt notR} theorem, 61
+  \item {\tt null} constant, 28
 
   \indexspace
 
-  \item {\textit {o}} type, 55
-  \item {\tt o} symbol, 2, 13
-  \item {\tt o_def} theorem, 6
-  \item {\tt of} symbol, 5
-  \item {\tt or_def} theorem, 6
-  \item {\tt Ord} theory, 3
-  \item {\tt ord} class, 3, 4, 22
-  \item {\tt order} class, 3, 22
+  \item {\textit {o}} type, 58
+  \item {\tt o} symbol, 6, 17
+  \item {\tt o_def} theorem, 10
+  \item {\tt of} symbol, 9
+  \item {\tt or_def} theorem, 10
+  \item {\tt Ord} theory, 7
+  \item {\tt ord} class, 7, 8, 26
+  \item {\tt order} class, 7, 26
 
   \indexspace
 
-  \item {\tt pack} ML type, 61
-  \item {\tt Pair} constant, 19
-  \item {\tt pair} constant, 69
-  \item {\tt Pair_eq} theorem, 19
-  \item {\tt Pair_inject} theorem, 19
-  \item {\tt PairE} theorem, 19
-  \item {\tt pc_tac}, \bold{63}, \bold{79}, 85, 86
-  \item {\tt plus} class, 3
-  \item {\tt PlusC_inl} theorem, 75
-  \item {\tt PlusC_inr} theorem, 75
-  \item {\tt PlusE} theorem, 75, 79, 83
-  \item {\tt PlusEL} theorem, 75
-  \item {\tt PlusF} theorem, 75
-  \item {\tt PlusFL} theorem, 75
-  \item {\tt PlusI_inl} theorem, 75, 84
-  \item {\tt PlusI_inlL} theorem, 75
-  \item {\tt PlusI_inr} theorem, 75
-  \item {\tt PlusI_inrL} theorem, 75
-  \item {\tt Pow} constant, 10
-  \item {\tt Pow_def} theorem, 13
-  \item {\tt PowD} theorem, 15
-  \item {\tt PowI} theorem, 15
-  \item {\tt primrec}, 41--44
-  \item {\tt primrec} symbol, 22
-  \item {\tt PROD} symbol, 70, 71
-  \item {\tt Prod} constant, 69
-  \item {\tt Prod} theory, 19
-  \item {\tt ProdC} theorem, 73, 89
-  \item {\tt ProdC2} theorem, 73
-  \item {\tt ProdE} theorem, 73, 86, 88, 90
-  \item {\tt ProdEL} theorem, 73
-  \item {\tt ProdF} theorem, 73
-  \item {\tt ProdFL} theorem, 73
-  \item {\tt ProdI} theorem, 73, 79, 81
-  \item {\tt ProdIL} theorem, 73
-  \item {\tt prop_cs}, \bold{18}
-  \item {\tt prop_pack}, \bold{62}
+  \item {\tt pack} ML type, 64
+  \item {\tt Pair} constant, 23
+  \item {\tt pair} constant, 72
+  \item {\tt Pair_eq} theorem, 23
+  \item {\tt Pair_inject} theorem, 23
+  \item {\tt PairE} theorem, 23
+  \item {\tt pc_tac}, \bold{66}, \bold{82}, 88, 89
+  \item {\tt plus} class, 7
+  \item {\tt PlusC_inl} theorem, 78
+  \item {\tt PlusC_inr} theorem, 78
+  \item {\tt PlusE} theorem, 78, 82, 86
+  \item {\tt PlusEL} theorem, 78
+  \item {\tt PlusF} theorem, 78
+  \item {\tt PlusFL} theorem, 78
+  \item {\tt PlusI_inl} theorem, 78, 87
+  \item {\tt PlusI_inlL} theorem, 78
+  \item {\tt PlusI_inr} theorem, 78
+  \item {\tt PlusI_inrL} theorem, 78
+  \item {\tt Pow} constant, 14
+  \item {\tt Pow_def} theorem, 17
+  \item {\tt PowD} theorem, 19
+  \item {\tt PowI} theorem, 19
+  \item {\tt primrec}, 45--48
+  \item {\tt primrec} symbol, 26
+  \item priorities, 3
+  \item {\tt PROD} symbol, 73, 74
+  \item {\tt Prod} constant, 72
+  \item {\tt Prod} theory, 23
+  \item {\tt ProdC} theorem, 76, 92
+  \item {\tt ProdC2} theorem, 76
+  \item {\tt ProdE} theorem, 76, 89, 91, 93
+  \item {\tt ProdEL} theorem, 76
+  \item {\tt ProdF} theorem, 76
+  \item {\tt ProdFL} theorem, 76
+  \item {\tt ProdI} theorem, 76, 82, 84
+  \item {\tt ProdIL} theorem, 76
+  \item {\tt prop_cs}, \bold{22}
+  \item {\tt prop_pack}, \bold{65}
 
   \indexspace
 
-  \item {\tt qed_spec_mp}, 39
+  \item {\tt qed_spec_mp}, 43
 
   \indexspace
 
-  \item {\tt range} constant, 10, 52
-  \item {\tt range_def} theorem, 13
-  \item {\tt rangeE} theorem, 15, 53
-  \item {\tt rangeI} theorem, 15
-  \item {\tt rec} constant, 69, 72
-  \item {\tt recdef}, 44--47
-  \item {\tt record}, 29
-  \item {\tt record_split_tac}, 31, 32
+  \item {\tt range} constant, 14, 56
+  \item {\tt range_def} theorem, 17
+  \item {\tt rangeE} theorem, 19, 56
+  \item {\tt rangeI} theorem, 19
+  \item {\tt rec} constant, 72, 75
+  \item {\tt recdef}, 48--51
+  \item {\tt record}, 33
+  \item {\tt record_split_tac}, 35, 36
   \item recursion
-    \subitem general, 44--47
-    \subitem primitive, 41--44
-  \item recursive functions, \see{recursion}{40}
-  \item {\tt red_if_equal} theorem, 72
-  \item {\tt Reduce} constant, 69, 72, 78
-  \item {\tt refl} theorem, 5, 58
-  \item {\tt refl_elem} theorem, 72, 76
-  \item {\tt refl_red} theorem, 72
-  \item {\tt refl_type} theorem, 72, 76
-  \item {\tt REPEAT_FIRST}, 77
-  \item {\tt repeat_goal_tac}, \bold{63}
-  \item {\tt replace_type} theorem, 76, 88
-  \item {\tt reresolve_tac}, \bold{63}
-  \item {\tt res_inst_tac}, 4
-  \item {\tt rev} constant, 24
-  \item {\tt rew_tac}, \bold{78}
-  \item {\tt RL}, 83
-  \item {\tt RS}, 88, 90
+    \subitem general, 48--51
+    \subitem primitive, 45--48
+  \item recursive functions, \see{recursion}{44}
+  \item {\tt red_if_equal} theorem, 75
+  \item {\tt Reduce} constant, 72, 75, 81
+  \item {\tt refl} theorem, 9, 61
+  \item {\tt refl_elem} theorem, 75, 79
+  \item {\tt refl_red} theorem, 75
+  \item {\tt refl_type} theorem, 75, 79
+  \item {\tt REPEAT_FIRST}, 80
+  \item {\tt repeat_goal_tac}, \bold{66}
+  \item {\tt replace_type} theorem, 79, 91
+  \item {\tt reresolve_tac}, \bold{66}
+  \item {\tt res_inst_tac}, 8
+  \item {\tt rev} constant, 28
+  \item {\tt rew_tac}, \bold{81}
+  \item {\tt RL}, 86
+  \item {\tt RS}, 91, 93
 
   \indexspace
 
-  \item {\tt safe_goal_tac}, \bold{63}
-  \item {\tt safe_tac}, \bold{79}
-  \item {\tt safestep_tac}, \bold{79}
+  \item {\tt safe_goal_tac}, \bold{66}
+  \item {\tt safe_tac}, \bold{82}
+  \item {\tt safestep_tac}, \bold{82}
   \item search
-    \subitem best-first, 54
-  \item {\tt select_equality} theorem, 6, 8
-  \item {\tt selectI} theorem, 5, 6
-  \item {\tt Seqof} constant, 56
-  \item sequent calculus, 55--67
-  \item {\tt Set} theory, 9, 12
-  \item {\tt set} constant, 24
-  \item {\tt set} type, 9
-  \item {\tt set_current_thy}, 54
-  \item {\tt set_diff_def} theorem, 13
-  \item {\tt show_sorts}, 4
-  \item {\tt show_types}, 4
-  \item {\tt Sigma} constant, 19
-  \item {\tt Sigma_def} theorem, 19
-  \item {\tt SigmaE} theorem, 19
-  \item {\tt SigmaI} theorem, 19
+    \subitem best-first, 57
+  \item {\tt select_equality} theorem, 10, 12
+  \item {\tt selectI} theorem, 9, 10
+  \item {\tt Seqof} constant, 59
+  \item sequent calculus, 58--70
+  \item {\tt Set} theory, 13, 16
+  \item {\tt set} constant, 28
+  \item {\tt set} type, 13
+  \item {\tt set_current_thy}, 57
+  \item {\tt set_diff_def} theorem, 17
+  \item {\tt show_sorts}, 8
+  \item {\tt show_types}, 8
+  \item {\tt Sigma} constant, 23
+  \item {\tt Sigma_def} theorem, 23
+  \item {\tt SigmaE} theorem, 23
+  \item {\tt SigmaI} theorem, 23
   \item simplification
-    \subitem of conjunctions, 17
-  \item {\tt size} constant, 35
-  \item {\tt snd} constant, 19, 69, 74
-  \item {\tt snd_conv} theorem, 19
-  \item {\tt snd_def} theorem, 74
-  \item {\tt sobj} type, 59
-  \item {\tt spec} theorem, 8
-  \item {\tt split} constant, 19, 69, 83
-  \item {\tt split} theorem, 19
-  \item {\tt split_all_tac}, \bold{20}
-  \item {\tt split_if} theorem, 8, 18
-  \item {\tt split_list_case} theorem, 23
-  \item {\tt split_split} theorem, 19
-  \item {\tt split_sum_case} theorem, 21
-  \item {\tt ssubst} theorem, 7, 9
-  \item {\tt stac}, \bold{17}
-  \item {\tt step_tac}, \bold{63}, \bold{79}
-  \item {\tt strip_tac}, \bold{9}
-  \item {\tt subset_def} theorem, 13
-  \item {\tt subset_refl} theorem, 14
-  \item {\tt subset_trans} theorem, 14
-  \item {\tt subsetCE} theorem, 12, 14
-  \item {\tt subsetD} theorem, 12, 14
-  \item {\tt subsetI} theorem, 14
-  \item {\tt subst} theorem, 5
-  \item {\tt subst_elem} theorem, 72
-  \item {\tt subst_elemL} theorem, 72
-  \item {\tt subst_eqtyparg} theorem, 76, 88
-  \item {\tt subst_prodE} theorem, 74, 76
-  \item {\tt subst_type} theorem, 72
-  \item {\tt subst_typeL} theorem, 72
-  \item {\tt Suc} constant, 21
-  \item {\tt Suc_not_Zero} theorem, 21
-  \item {\tt succ} constant, 69
-  \item {\tt SUM} symbol, 70, 71
-  \item {\tt Sum} constant, 69
-  \item {\tt Sum} theory, 20
-  \item {\tt sum_case} constant, 21
-  \item {\tt sum_case_Inl} theorem, 21
-  \item {\tt sum_case_Inr} theorem, 21
-  \item {\tt SumC} theorem, 74
-  \item {\tt SumE} theorem, 74, 79, 83
-  \item {\tt sumE} theorem, 21
-  \item {\tt SumE_fst} theorem, 74, 76, 88, 89
-  \item {\tt SumE_snd} theorem, 74, 76, 90
-  \item {\tt SumEL} theorem, 74
-  \item {\tt SumF} theorem, 74
-  \item {\tt SumFL} theorem, 74
-  \item {\tt SumI} theorem, 74, 84
-  \item {\tt SumIL} theorem, 74
-  \item {\tt SumIL2} theorem, 76
-  \item {\tt surj} constant, 13, 17
-  \item {\tt surj_def} theorem, 17
-  \item {\tt surjective_pairing} theorem, 19
-  \item {\tt surjective_sum} theorem, 21
-  \item {\tt swap} theorem, 8
-  \item {\tt swap_res_tac}, 53
-  \item {\tt sym} theorem, 7, 58
-  \item {\tt sym_elem} theorem, 72
-  \item {\tt sym_type} theorem, 72
-  \item {\tt symL} theorem, 59
+    \subitem of conjunctions, 21
+  \item {\tt size} constant, 40
+  \item {\tt snd} constant, 23, 72, 77
+  \item {\tt snd_conv} theorem, 23
+  \item {\tt snd_def} theorem, 77
+  \item {\tt sobj} type, 62
+  \item {\tt spec} theorem, 12
+  \item {\tt split} constant, 23, 72, 86
+  \item {\tt split} theorem, 23
+  \item {\tt split_all_tac}, \bold{24}
+  \item {\tt split_if} theorem, 12, 22
+  \item {\tt split_list_case} theorem, 27
+  \item {\tt split_split} theorem, 23
+  \item {\tt split_sum_case} theorem, 25
+  \item {\tt ssubst} theorem, 11, 13
+  \item {\tt stac}, \bold{21}
+  \item {\tt step_tac}, \bold{66}, \bold{82}
+  \item {\tt strip_tac}, \bold{13}
+  \item {\tt subset_def} theorem, 17
+  \item {\tt subset_refl} theorem, 18
+  \item {\tt subset_trans} theorem, 18
+  \item {\tt subsetCE} theorem, 16, 18
+  \item {\tt subsetD} theorem, 16, 18
+  \item {\tt subsetI} theorem, 18
+  \item {\tt subst} theorem, 9
+  \item {\tt subst_elem} theorem, 75
+  \item {\tt subst_elemL} theorem, 75
+  \item {\tt subst_eqtyparg} theorem, 79, 91
+  \item {\tt subst_prodE} theorem, 77, 79
+  \item {\tt subst_type} theorem, 75
+  \item {\tt subst_typeL} theorem, 75
+  \item {\tt Suc} constant, 25
+  \item {\tt Suc_not_Zero} theorem, 25
+  \item {\tt succ} constant, 72
+  \item {\tt SUM} symbol, 73, 74
+  \item {\tt Sum} constant, 72
+  \item {\tt Sum} theory, 24
+  \item {\tt sum_case} constant, 25
+  \item {\tt sum_case_Inl} theorem, 25
+  \item {\tt sum_case_Inr} theorem, 25
+  \item {\tt SumC} theorem, 77
+  \item {\tt SumE} theorem, 77, 82, 86
+  \item {\tt sumE} theorem, 25
+  \item {\tt SumE_fst} theorem, 77, 79, 91, 92
+  \item {\tt SumE_snd} theorem, 77, 79, 93
+  \item {\tt SumEL} theorem, 77
+  \item {\tt SumF} theorem, 77
+  \item {\tt SumFL} theorem, 77
+  \item {\tt SumI} theorem, 77, 87
+  \item {\tt SumIL} theorem, 77
+  \item {\tt SumIL2} theorem, 79
+  \item {\tt surj} constant, 17, 21
+  \item {\tt surj_def} theorem, 21
+  \item {\tt surjective_pairing} theorem, 23
+  \item {\tt surjective_sum} theorem, 25
+  \item {\tt swap} theorem, 12
+  \item {\tt swap_res_tac}, 57
+  \item {\tt sym} theorem, 11, 61
+  \item {\tt sym_elem} theorem, 75
+  \item {\tt sym_type} theorem, 75
+  \item {\tt symL} theorem, 62
 
   \indexspace
 
-  \item {\tt T} constant, 69
-  \item {\textit {t}} type, 68
-  \item {\tt take} constant, 24
-  \item {\tt takeWhile} constant, 24
-  \item {\tt TC} theorem, 75
-  \item {\tt TE} theorem, 75
-  \item {\tt TEL} theorem, 75
-  \item {\tt term} class, 3, 55
-  \item {\tt test_assume_tac}, \bold{77}
-  \item {\tt TF} theorem, 75
-  \item {\tt THE} symbol, 56
-  \item {\tt The} constant, 56
-  \item {\tt The} theorem, 58
-  \item {\tt thinL} theorem, 58
-  \item {\tt thinR} theorem, 58
-  \item {\tt TI} theorem, 75
-  \item {\tt times} class, 3
-  \item {\tt tl} constant, 24
+  \item {\tt T} constant, 72
+  \item {\textit {t}} type, 71
+  \item {\tt take} constant, 28
+  \item {\tt takeWhile} constant, 28
+  \item {\tt TC} theorem, 78
+  \item {\tt TE} theorem, 78
+  \item {\tt TEL} theorem, 78
+  \item {\tt term} class, 7, 58
+  \item {\tt test_assume_tac}, \bold{80}
+  \item {\tt TF} theorem, 78
+  \item {\tt THE} symbol, 59
+  \item {\tt The} constant, 59
+  \item {\tt The} theorem, 61
+  \item {\tt thinL} theorem, 61
+  \item {\tt thinR} theorem, 61
+  \item {\tt TI} theorem, 78
+  \item {\tt times} class, 7
+  \item {\tt tl} constant, 28
   \item tracing
-    \subitem of unification, 4
-  \item {\tt trans} theorem, 7, 58
-  \item {\tt trans_elem} theorem, 72
-  \item {\tt trans_red} theorem, 72
-  \item {\tt trans_tac}, 23
-  \item {\tt trans_type} theorem, 72
-  \item {\tt True} constant, 2, 56
-  \item {\tt True_def} theorem, 6, 58
-  \item {\tt True_or_False} theorem, 5, 6
-  \item {\tt TrueI} theorem, 7
-  \item {\tt Trueprop} constant, 2, 56
-  \item {\tt TrueR} theorem, 59
-  \item {\tt tt} constant, 69
-  \item {\tt Type} constant, 69
-  \item type definition, \bold{26}
-  \item {\tt typechk_tac}, \bold{77}, 82, 85, 89, 90
-  \item {\tt typedef}, 23
+    \subitem of unification, 8
+  \item {\tt trans} theorem, 11, 61
+  \item {\tt trans_elem} theorem, 75
+  \item {\tt trans_red} theorem, 75
+  \item {\tt trans_tac}, 27
+  \item {\tt trans_type} theorem, 75
+  \item {\tt True} constant, 6, 59
+  \item {\tt True_def} theorem, 10, 61
+  \item {\tt True_or_False} theorem, 9, 10
+  \item {\tt TrueI} theorem, 11
+  \item {\tt Trueprop} constant, 6, 59
+  \item {\tt TrueR} theorem, 62
+  \item {\tt tt} constant, 72
+  \item {\tt Type} constant, 72
+  \item type definition, \bold{30}
+  \item {\tt typechk_tac}, \bold{80}, 85, 88, 92, 93
+  \item {\tt typedef}, 27
 
   \indexspace
 
-  \item {\tt UN} symbol, 10--12
-  \item {\tt Un} symbol, 10
-  \item {\tt Un1} theorem, 12
-  \item {\tt Un2} theorem, 12
-  \item {\tt Un_absorb} theorem, 16
-  \item {\tt Un_assoc} theorem, 16
-  \item {\tt Un_commute} theorem, 16
-  \item {\tt Un_def} theorem, 13
-  \item {\tt UN_E} theorem, 15
-  \item {\tt UN_I} theorem, 15
-  \item {\tt Un_Int_distrib} theorem, 16
-  \item {\tt Un_Inter} theorem, 16
-  \item {\tt Un_least} theorem, 16
-  \item {\tt Un_Union_image} theorem, 16
-  \item {\tt Un_upper1} theorem, 16
-  \item {\tt Un_upper2} theorem, 16
-  \item {\tt UnCI} theorem, 12, 15
-  \item {\tt UnE} theorem, 15
-  \item {\tt UnI1} theorem, 15
-  \item {\tt UnI2} theorem, 15
+  \item {\tt UN} symbol, 14--16
+  \item {\tt Un} symbol, 14
+  \item {\tt Un1} theorem, 16
+  \item {\tt Un2} theorem, 16
+  \item {\tt Un_absorb} theorem, 20
+  \item {\tt Un_assoc} theorem, 20
+  \item {\tt Un_commute} theorem, 20
+  \item {\tt Un_def} theorem, 17
+  \item {\tt UN_E} theorem, 19
+  \item {\tt UN_I} theorem, 19
+  \item {\tt Un_Int_distrib} theorem, 20
+  \item {\tt Un_Inter} theorem, 20
+  \item {\tt Un_least} theorem, 20
+  \item {\tt Un_Union_image} theorem, 20
+  \item {\tt Un_upper1} theorem, 20
+  \item {\tt Un_upper2} theorem, 20
+  \item {\tt UnCI} theorem, 16, 19
+  \item {\tt UnE} theorem, 19
+  \item {\tt UnI1} theorem, 19
+  \item {\tt UnI2} theorem, 19
   \item unification
-    \subitem incompleteness of, 4
-  \item {\tt Unify.trace_types}, 4
-  \item {\tt UNION} constant, 10
-  \item {\tt Union} constant, 10
-  \item {\tt UNION1} constant, 10
-  \item {\tt UNION1_def} theorem, 13
-  \item {\tt UNION_def} theorem, 13
-  \item {\tt Union_def} theorem, 13
-  \item {\tt Union_least} theorem, 16
-  \item {\tt Union_Un_distrib} theorem, 16
-  \item {\tt Union_upper} theorem, 16
-  \item {\tt UnionE} theorem, 15
-  \item {\tt UnionI} theorem, 15
-  \item {\tt unit_eq} theorem, 20
+    \subitem incompleteness of, 8
+  \item {\tt Unify.trace_types}, 8
+  \item {\tt UNION} constant, 14
+  \item {\tt Union} constant, 14
+  \item {\tt UNION1} constant, 14
+  \item {\tt UNION1_def} theorem, 17
+  \item {\tt UNION_def} theorem, 17
+  \item {\tt Union_def} theorem, 17
+  \item {\tt Union_least} theorem, 20
+  \item {\tt Union_Un_distrib} theorem, 20
+  \item {\tt Union_upper} theorem, 20
+  \item {\tt UnionE} theorem, 19
+  \item {\tt UnionI} theorem, 19
+  \item {\tt unit_eq} theorem, 24
 
   \indexspace
 
-  \item {\tt when} constant, 69, 74, 83
+  \item {\tt when} constant, 72, 77, 86
 
   \indexspace
 
-  \item {\tt zero_ne_succ} theorem, 72, 73
-  \item {\tt ZF} theory, 1
+  \item {\tt zero_ne_succ} theorem, 75, 76
+  \item {\tt ZF} theory, 5
 
 \end{theindex}

--- a/doc-src/ZF/ZF.tex	Tue Jan 19 11:16:39 1999 +0100
+++ b/doc-src/ZF/ZF.tex	Tue Jan 19 11:18:11 1999 +0100
@@ -1669,7 +1669,7 @@
 val free_iffs     : thm list  \textrm{logical equivalences for proving freeness}
 val free_SEs      : thm list  \textrm{elimination rules for proving freeness}
 val mk_free       : string -> thm  \textrm{A function for proving freeness theorems}
-val mk_cases      : thm list -> string -> thm  \textrm{case analysis, see below}
+val mk_cases      : string -> thm  \textrm{case analysis, see below}
 val defs          : thm list  \textrm{definitions of operators}
 val bnd_mono      : thm list  \textrm{monotonicity property}
 val dom_subset    : thm list  \textrm{inclusion in `bounding set'}
@@ -1746,13 +1746,12 @@
 {\out                     ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm}
 \end{ttbox}
 
-The purpose of \ttindex{mk_cases} is to generate simplified instances of the
-elimination (case analysis) rule.  Its theorem list argument is a list of
-constructor definitions, which it uses for freeness reasoning.  For example,
-this instance of the elimination rule propagates type-checking information
-from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$:
+The purpose of \ttindex{mk_cases} is to generate instances of the elimination
+(case analysis) rule that have been simplified using freeness reasoning.  For
+example, this instance of the elimination rule propagates type-checking
+information from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$:
 \begin{ttbox}
-val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)";
+val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
 {\out val BrE =}
 {\out   "[| Br(?a, ?l, ?r) : bt(?A);}
 {\out       [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm}
@@ -2130,7 +2129,7 @@
 \begin{ttbox}
 val intrs         : thm list  \textrm{the introduction rules}
 val elim          : thm       \textrm{the elimination (case analysis) rule}
-val mk_cases      : thm list -> string -> thm  \textrm{case analysis, see below}
+val mk_cases      : string -> thm  \textrm{case analysis, see below}
 val induct        : thm       \textrm{the standard induction rule}
 val mutual_induct : thm       \textrm{the mutual induction rule, or \texttt{True}}
 val defs          : thm list  \textrm{definitions of operators}
@@ -2160,7 +2159,7 @@
 inductively.  Then the file \texttt{ex/Comb.ML} defines special cases of
 contraction using \texttt{mk_cases}:
 \begin{ttbox}
-val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
+val K_contractE = contract.mk_cases "K -1-> r";
 {\out val K_contractE = "K -1-> ?r ==> ?Q" : thm}
 \end{ttbox}
 We can read this as saying that the combinator \texttt{K} cannot reduce to

--- a/src/HOL/Auth/Message.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Auth/Message.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -576,16 +576,12 @@
 
 AddIs  synth.intrs;
 
-(*Can only produce a nonce or key if it is already known,
-  but can synth a pair or encryption from its components...*)
-val mk_cases = synth.mk_cases (atomic.simps @ msg.simps);
-
 (*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
-val Nonce_synth = mk_cases "Nonce n : synth H";
-val Key_synth   = mk_cases "Key K : synth H";
-val Hash_synth  = mk_cases "Hash X : synth H";
-val MPair_synth = mk_cases "{|X,Y|} : synth H";
-val Crypt_synth = mk_cases "Crypt K X : synth H";
+val Nonce_synth = synth.mk_cases "Nonce n : synth H";
+val Key_synth   = synth.mk_cases "Key K : synth H";
+val Hash_synth  = synth.mk_cases "Hash X : synth H";
+val MPair_synth = synth.mk_cases "{|X,Y|} : synth H";
+val Crypt_synth = synth.mk_cases "Crypt K X : synth H";
 
 AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
 

--- a/src/HOL/Finite.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Finite.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -325,9 +325,9 @@
 Addsimps [card_insert_disjoint];
 *)
 
-val cardR_emptyE = cardR.mk_cases [] "({},n) : cardR";
+val cardR_emptyE = cardR.mk_cases "({},n) : cardR";
 AddSEs [cardR_emptyE];
-val cardR_insertE = cardR.mk_cases [] "(insert a A,n) : cardR";
+val cardR_insertE = cardR.mk_cases "(insert a A,n) : cardR";
 AddSIs cardR.intrs;
 
 Goal "[| (A,n) : cardR |] ==> a : A --> (? m. n = Suc m)";
@@ -565,7 +565,7 @@
 
 (*** foldSet ***)
 
-val empty_foldSetE = foldSet.mk_cases [] "({}, x) : foldSet f e";
+val empty_foldSetE = foldSet.mk_cases "({}, x) : foldSet f e";
 
 AddSEs [empty_foldSetE];
 AddIs foldSet.intrs;

--- a/src/HOL/IMP/Expr.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/IMP/Expr.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -7,16 +7,21 @@
 Not used in the rest of the language, but included for completeness.
 *)
 
-val evala_elim_cases = map (evala.mk_cases aexp.simps)
-   ["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i",
-    "(Op1 f e,sigma) -a-> i", "(Op2 f a1 a2,sigma)  -a-> i"
-   ];
+val evala_elim_cases = 
+    map evala.mk_cases
+       ["(N(n),sigma) -a-> i", 
+	"(X(x),sigma) -a-> i",
+	"(Op1 f e,sigma) -a-> i", 
+	"(Op2 f a1 a2,sigma)  -a-> i"];
 
-val evalb_elim_cases = map (evalb.mk_cases bexp.simps)
-   ["(true,sigma) -b-> x", "(false,sigma) -b-> x",
-    "(ROp f a0 a1,sigma) -b-> x", "(noti(b),sigma) -b-> x",
-    "(b0 andi b1,sigma) -b-> x", "(b0 ori b1,sigma) -b-> x"
-   ];
+val evalb_elim_cases = 
+    map evalb.mk_cases
+       ["(true,sigma) -b-> x", 
+	"(false,sigma) -b-> x",
+	"(ROp f a0 a1,sigma) -b-> x", 
+	"(noti(b),sigma) -b-> x",
+	"(b0 andi b1,sigma) -b-> x", 
+	"(b0 ori b1,sigma) -b-> x"];
 
 val evalb_simps = map (fn s => prove_goal Expr.thy s
     (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))

--- a/src/HOL/IMP/Natural.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/IMP/Natural.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -8,11 +8,14 @@
 
 AddIs evalc.intrs;
 
-val evalc_elim_cases = map (evalc.mk_cases com.simps)
-   ["<SKIP,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
-    "<IF b THEN c1 ELSE c2, s> -c-> t"];
+val evalc_elim_cases = 
+    map evalc.mk_cases
+       ["<SKIP,s> -c-> t", 
+	"<x:=a,s> -c-> t", 
+	"<c1;c2, s> -c-> t",
+	"<IF b THEN c1 ELSE c2, s> -c-> t"];
 
-val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t";
+val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
 
 AddSEs evalc_elim_cases;
 

--- a/src/HOL/IMP/Transition.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/IMP/Transition.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -10,11 +10,14 @@
 
 AddSEs [rel_pow_0_E];
 
-val evalc1_SEs = map (evalc1.mk_cases com.simps)
-   ["(SKIP,s) -1-> t", "(x:=a,s) -1-> t","(c1;c2, s) -1-> t", 
-    "(IF b THEN c1 ELSE c2, s) -1-> t"];
-val evalc1_Es = map (evalc1.mk_cases com.simps)
-   ["(WHILE b DO c,s) -1-> t"];
+val evalc1_SEs = 
+    map evalc1.mk_cases
+       ["(SKIP,s) -1-> t", 
+	"(x:=a,s) -1-> t",
+	"(c1;c2, s) -1-> t", 
+	"(IF b THEN c1 ELSE c2, s) -1-> t"];
+
+val evalc1_E = evalc1.mk_cases "(WHILE b DO c,s) -1-> t";
 
 AddSEs evalc1_SEs;
 
@@ -95,7 +98,7 @@
 by (strip_tac 1);
 by (etac rel_pow_E2 1);
  by (Asm_full_simp_tac 1);
-by (eresolve_tac evalc1_Es 1);
+by (etac evalc1_E 1);
 
 (* WhileFalse *)
  by (fast_tac (claset() addSDs [hlemma]) 1);

--- a/src/HOL/Induct/Com.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Induct/Com.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -8,11 +8,14 @@
 
 AddIs exec.intrs;
 
-val exec_elim_cases = map (exec.mk_cases exp.simps)
-   ["(SKIP,s) -[eval]-> t", "(x:=a,s) -[eval]-> t", "(c1;;c2, s) -[eval]-> t",
-    "(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
+val exec_elim_cases = 
+    map exec.mk_cases
+       ["(SKIP,s) -[eval]-> t",
+	"(x:=a,s) -[eval]-> t", 
+	"(c1;;c2, s) -[eval]-> t",
+	"(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
 
-val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) -[eval]-> t";
+val exec_WHILE_case = exec.mk_cases "(WHILE b DO c,s) -[eval]-> t";
 
 AddSEs exec_elim_cases;
 

--- a/src/HOL/Induct/Comb.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Induct/Comb.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -45,9 +45,9 @@
 (*** Results about Contraction ***)
 
 (*Derive a case for each combinator constructor*)
-val K_contractE = contract.mk_cases comb.simps "K -1-> z";
-val S_contractE = contract.mk_cases comb.simps "S -1-> z";
-val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
+val K_contractE  = contract.mk_cases "K -1-> z";
+val S_contractE  = contract.mk_cases "S -1-> z";
+val Ap_contractE = contract.mk_cases "x#y -1-> z";
 
 AddSIs [contract.K, contract.S];
 AddIs  [contract.Ap1, contract.Ap2];
@@ -96,9 +96,9 @@
 (*** Results about Parallel Contraction ***)
 
 (*Derive a case for each combinator constructor*)
-val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
-val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
-val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
+val K_parcontractE  = parcontract.mk_cases "K =1=> z";
+val S_parcontractE  = parcontract.mk_cases "S =1=> z";
+val Ap_parcontractE = parcontract.mk_cases "x#y =1=> z";
 
 AddSIs [parcontract.refl, parcontract.K, parcontract.S];
 AddIs  [parcontract.Ap];

--- a/src/HOL/Induct/Exp.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Induct/Exp.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -9,11 +9,12 @@
 AddSIs [eval.N, eval.X];
 AddIs  [eval.Op, eval.valOf];
 
-val eval_elim_cases = map (eval.mk_cases exp.simps)
-   ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
-    "(Op f a1 a2,sigma)  -|-> (n,s')",
-    "(VALOF c RESULTIS e, s) -|-> (n, s1)"
-   ];
+val eval_elim_cases = 
+    map eval.mk_cases 
+       ["(N(n),sigma) -|-> (n',s')", 
+	"(X(x),sigma) -|-> (n,s')",
+	"(Op f a1 a2,sigma)  -|-> (n,s')",
+	"(VALOF c RESULTIS e, s) -|-> (n, s1)"];
 
 AddSEs eval_elim_cases;
 

--- a/src/HOL/Induct/LFilter.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Induct/LFilter.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -9,8 +9,7 @@
 
 (*** findRel: basic laws ****)
 
-val findRel_LConsE = 
-    findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p";
+val findRel_LConsE = findRel.mk_cases "(LCons x l, l'') : findRel p";
 
 AddSEs [findRel_LConsE];
 

--- a/src/HOL/Lambda/Eta.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Lambda/Eta.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -12,8 +12,7 @@
 Addsimps eta.intrs;
 AddIs eta.intrs;
 
-val eta_cases = map (eta.mk_cases dB.simps)
-    ["Abs s -e> z","s $ t -e> u","Var i -e> t"];
+val eta_cases = map eta.mk_cases ["Abs s -e> z", "s $ t -e> u", "Var i -e> t"];
 AddSEs eta_cases;
 
 section "eta, subst and free";

--- a/src/HOL/Lambda/InductTermi.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Lambda/InductTermi.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -43,48 +43,27 @@
 
 (*** Every terminating term is in IT ***)
 
-val IT_cases = map (IT.mk_cases
- ([Var_apps_eq_Var_apps_conv, Abs_eq_apps_conv, apps_eq_Abs_conv,
-   Abs_apps_eq_Abs_apps_conv,
-   Var_apps_neq_Abs_apps, Var_apps_neq_Abs_apps RS not_sym,
-   hd(tl(get_thms List.thy "foldl.simps")) RS sym ]
-  @ dB.simps @ list.simps))
-    ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"];
+Addsimps [Var_apps_neq_Abs_apps RS not_sym];
+
+Goal "Var n $$ ss ~= Abs r $ s $$ ts";
+by (simp_tac (simpset() addsimps [foldl_Cons RS sym] 
+	                delsimps [foldl_Cons]) 1);
+qed "Var_apps_neq_Abs_app_apps";
+Addsimps [Var_apps_neq_Abs_app_apps,
+	  Var_apps_neq_Abs_app_apps RS not_sym];
+
+
+Goal "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r=r' & s=s' & ss=ss')";
+by (simp_tac (simpset() addsimps [foldl_Cons RS sym] 
+	                delsimps [foldl_Cons]) 1);
+qed "Abs_apps_eq_Abs_app_apps";
+Addsimps [Abs_apps_eq_Abs_app_apps];
+
+val IT_cases = 
+    map IT.mk_cases
+        ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"];
 AddSEs IT_cases;
 
-(* Turned out to be redundant:
-Goal "t : termi beta ==> \
-\     !r rs. t = r$$rs --> r : termi beta & rs : termi(step1 beta)";
-by (etac acc_induct 1);
-by (force_tac (claset()
-     addIs [apps_preserves_beta,apps_preserves_betas,accI],simpset()) 1);
-val lemma = result();
-
-Goal "r$$rs : termi beta ==> r : termi beta & rs : termi(step1 beta)";
-by (dtac lemma 1);
-by (Blast_tac 1);
-qed "apps_in_termi_betaD";
-
-Goal "t : termi beta ==> !r. t = Abs r --> r : termi beta";
-by (etac acc_induct 1);
-by (force_tac (claset() addIs [accI],simpset()) 1);
-val lemma = result();
-
-Goal "Abs r : termi beta ==> r : termi beta";
-by (dtac lemma 1);
-by (Blast_tac 1);
-qed "Abs_in_termi_betaD";
-
-Goal "t : termi beta ==> !r s. t = r$s --> r : termi beta & s : termi beta";
-by (etac acc_induct 1);
-by (force_tac (claset() addIs [accI],simpset()) 1);
-val lemma = result();
-
-Goal "r$s : termi beta ==> r : termi beta & s : termi beta";
-by (dtac lemma 1);
-by (Blast_tac 1);
-qed "App_in_termi_betaD";
-*)
 
 Goal "r : termi beta ==> r : IT";
 by (etac acc_induct 1);

--- a/src/HOL/Lambda/Lambda.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -8,8 +8,7 @@
 
 (*** Lambda ***)
 
-val beta_cases = map (beta.mk_cases dB.simps)
-    ["Var i -> t", "Abs r -> s", "s $ t -> u"];
+val beta_cases = map beta.mk_cases ["Var i -> t", "Abs r -> s", "s $ t -> u"];
 AddSEs beta_cases;
 
 Delsimps [subst_Var];

--- a/src/HOL/Lambda/ParRed.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Lambda/ParRed.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -7,13 +7,15 @@
 confluence of beta.
 *)
 
-open ParRed;
-
 Addsimps par_beta.intrs;
 
-val par_beta_cases = map (par_beta.mk_cases dB.simps)
-    ["Var n => t", "Abs s => Abs t",
-     "(Abs s) $ t => u", "s $ t => u", "Abs s => t"];
+val par_beta_cases = 
+    map par_beta.mk_cases
+       ["Var n => t", 
+	"Abs s => Abs t",
+	"(Abs s) $ t => u", 
+	"s $ t => u", 
+	"Abs s => t"];
 
 AddSIs par_beta.intrs;
 AddSEs par_beta_cases;

--- a/src/HOL/List.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/List.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -32,7 +32,7 @@
 by (REPEAT (ares_tac basic_monos 1));
 qed "lists_mono";
 
-val listsE = lists.mk_cases list.simps  "x#l : lists A";
+val listsE = lists.mk_cases "x#l : lists A";
 AddSEs [listsE];
 AddSIs lists.intrs;
 

--- a/src/HOL/List.thy	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/List.thy	Tue Jan 19 11:18:11 1999 +0100
@@ -114,8 +114,8 @@
   "filter P [] = []"
   "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
 primrec
-  "foldl f a [] = a"
-  "foldl f a (x#xs) = foldl f (f a x) xs"
+  foldl_Nil  "foldl f a [] = a"
+  foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
 primrec
   "concat([]) = []"
   "concat(x#xs) = x @ concat(xs)"

--- a/src/HOL/MiniML/W.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/MiniML/W.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -6,16 +6,17 @@
 Correctness and completeness of type inference algorithm W
 *)
 
-open W;
-
 Addsimps [Suc_le_lessD];  Delsimps [less_imp_le];  (*the combination loops*)
 
-val has_type_casesE = map(has_type.mk_cases expr.simps)
-        [" A |- Var n :: t"," A |- Abs e :: t","A |- App e1 e2 ::t","A |- LET e1 e2 ::t" ];
+val has_type_casesE = 
+    map has_type.mk_cases
+	[" A |- Var n :: t",
+	 " A |- Abs e :: t",
+	 "A |- App e1 e2 ::t",
+	 "A |- LET e1 e2 ::t" ];
 
 (* the resulting type variable is always greater or equal than the given one *)
-Goal
-        "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
+Goal "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
 by (induct_tac "e" 1);
 (* case Var(n) *)
 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
@@ -32,8 +33,7 @@
 
 Addsimps [W_var_ge];
 
-Goal
-        "Some (S,t,m) = W e A n ==> n<=m";
+Goal "Some (S,t,m) = W e A n ==> n<=m";
 by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 qed "W_var_geD";
 
@@ -67,8 +67,7 @@
 Addsimps [new_tv_bound_typ_inst_sch];
 
 (* resulting type variable is new *)
-Goal
-     "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
+Goal "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
 \                 new_tv m S & new_tv m t";
 by (induct_tac "e" 1);
 (* case Var n *)
@@ -163,8 +162,7 @@
 
 Addsimps [free_tv_bound_typ_inst1];
 
-Goal
-     "!n A S t m v. W e A n = Some (S,t,m) -->            \
+Goal "!n A S t m v. W e A n = Some (S,t,m) -->            \
 \         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
 by (induct_tac "e" 1);
 (* case Var n *)
@@ -259,8 +257,7 @@
 val weaken_not_elem_A_minus_B = result();
 
 (* correctness of W with respect to has_type *)
-Goal
-        "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
+Goal "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
 by (induct_tac "e" 1);
 (* case Var n *)
 by (Asm_full_simp_tac 1);
@@ -380,8 +377,7 @@
 qed_spec_mp "W_correct_lemma";
 
 (* Completeness of W w.r.t. has_type *)
-Goal
- "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
+Goal "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
 \             (? S t. (? m. W e A n = Some (S,t,m)) &  \
 \                     (? R. $S' A = $R ($S A) & t' = $R t))";
 by (induct_tac "e" 1);
@@ -554,8 +550,7 @@
 by (simp_tac (simpset() addsimps [o_def,subst_comp_scheme_list RS sym]) 1);
 qed_spec_mp "W_complete_lemma";
 
-Goal
- "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
+Goal "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &  \
 \                                 (? R. t' = $ R t))";
 by (cut_inst_tac [("A","[]"),("S'","id_subst"),("e","e"),("t'","t'")]
                 W_complete_lemma 1);

--- a/src/HOL/Tools/inductive_package.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -34,13 +34,13 @@
     term list -> thm list -> thm list -> theory -> theory *
       {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
        intrs:thm list,
-       mk_cases:thm list -> string -> thm, mono:thm,
+       mk_cases:string -> thm, mono:thm,
        unfold:thm}
   val add_inductive : bool -> bool -> string list -> string list
     -> xstring list -> xstring list -> theory -> theory *
       {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
        intrs:thm list,
-       mk_cases:thm list -> string -> thm, mono:thm,
+       mk_cases:string -> thm, mono:thm,
        unfold:thm}
 end;
 
@@ -289,21 +289,21 @@
   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   for inference systems.
  *)
-fun con_elim_tac simps =
+fun con_elim_tac ss =
   let val elim_tac = REPEAT o (eresolve_tac elim_rls)
   in ALLGOALS(EVERY'[elim_tac,
-                 asm_full_simp_tac (simpset_of NatDef.thy addsimps simps),
-                 elim_tac,
-                 REPEAT o bound_hyp_subst_tac])
+		     asm_full_simp_tac ss,
+		     elim_tac,
+		     REPEAT o bound_hyp_subst_tac])
      THEN prune_params_tac
   end;
 
 (*String s should have the form t:Si where Si is an inductive set*)
-fun mk_cases elims simps s =
-  let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT));
-      val elims' = map (try (fn r =>
-        rule_by_tactic (con_elim_tac simps) (prem RS r) |> standard)) elims
-  in case find_first is_some elims' of
+fun mk_cases elims s =
+  let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT))
+      fun mk_elim rl = rule_by_tactic (con_elim_tac (simpset())) (prem RS rl) 
+	               |> standard
+  in case find_first is_some (map (try mk_elim) elims) of
        Some (Some r) => r
      | None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")
   end;

--- a/src/HOL/W0/W.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/W0/W.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -36,7 +36,7 @@
 by (asm_full_simp_tac (simpset() addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
 qed_spec_mp "W_correct";
 
-val has_type_casesE = map(has_type.mk_cases expr.simps)
+val has_type_casesE = map has_type.mk_cases
         [" s |- Var n :: t"," s |- Abs e :: t","s |- App e1 e2 ::t"];
 
 (* the resulting type variable is always greater or equal than the given one *)

--- a/src/ZF/Coind/ECR.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Coind/ECR.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -24,11 +24,9 @@
 
 (* Specialised elimination rules *)
 
-val htr_constE = 
-  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_const(c),t>:HasTyRel");
+val htr_constE = HasTyRel.mk_cases "<v_const(c),t>:HasTyRel";
 
-val htr_closE =
-  (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_clos(x,e,ve),t>:HasTyRel");
+val htr_closE = HasTyRel.mk_cases "<v_clos(x,e,ve),t>:HasTyRel";
 
 (* Classical reasoning sets *)
 

--- a/src/ZF/Coind/MT.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Coind/MT.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -55,7 +55,7 @@
 by (eres_inst_tac [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")] 
     (SigmaD1 RS te_owrE) 1);
 by (assume_tac 1);
-by (rtac ElabRel.elab_fnI 1);
+by (rtac ElabRel.fnI 1);
 by clean_tac;
 by (Asm_simp_tac 1);
 by (stac ve_dom_owr 1);
@@ -78,8 +78,7 @@
 qed "consistency_fix";
 
 
-Goal
-   "[| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
+Goal "[| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const;   \
 \     <ve,e1,v_const(c1)>:EvalRel;                      \
 \     ALL t te.                                         \
 \       hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \
@@ -93,25 +92,24 @@
 by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1);
 qed "consistency_app1";
 
-Goal
-   "[| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;  \
-\      <ve,e1,v_clos(xm,em,vem)>:EvalRel;       \
-\      ALL t te.                                \
-\        hastyenv(ve,te) -->                    \
-\        <te,e1,t>:ElabRel -->                  \
-\        <v_clos(xm,em,vem),t>:HasTyRel;        \
-\      <ve,e2,v2>:EvalRel;                      \
-\      ALL t te.                                \
-\        hastyenv(ve,te) -->                    \
-\        <te,e2,t>:ElabRel -->                  \
-\        <v2,t>:HasTyRel;                       \
-\      <ve_owr(vem,xm,v2),em,v>:EvalRel;        \
-\      ALL t te.                                \
-\        hastyenv(ve_owr(vem,xm,v2),te) -->     \
-\        <te,em,t>:ElabRel -->                  \
-\        <v,t>:HasTyRel;                        \
-\      hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==>      \
-\   <v,t>:HasTyRel ";
+Goal "[| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val;  \
+\        <ve,e1,v_clos(xm,em,vem)>:EvalRel;       \
+\        ALL t te.                                \
+\          hastyenv(ve,te) -->                    \
+\          <te,e1,t>:ElabRel -->                  \
+\          <v_clos(xm,em,vem),t>:HasTyRel;        \
+\        <ve,e2,v2>:EvalRel;                      \
+\        ALL t te.                                \
+\          hastyenv(ve,te) -->                    \
+\          <te,e2,t>:ElabRel -->                  \
+\          <v2,t>:HasTyRel;                       \
+\        <ve_owr(vem,xm,v2),em,v>:EvalRel;        \
+\        ALL t te.                                \
+\          hastyenv(ve_owr(vem,xm,v2),te) -->     \
+\          <te,em,t>:ElabRel -->                  \
+\          <v,t>:HasTyRel;                        \
+\        hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==>      \
+\     <v,t>:HasTyRel ";
 by (etac elab_appE 1);
 by (dtac (spec RS spec RS mp RS mp) 1);
 by (assume_tac 1);
@@ -121,8 +119,8 @@
 by (assume_tac 1);
 by (etac htr_closE 1);
 by (etac elab_fnE 1);
-by (rewrite_tac Ty.con_defs);
-by Safe_tac;
+by (Full_simp_tac 1);
+by (Clarify_tac 1);
 by (dtac (spec RS spec RS mp RS mp) 1);
 by (assume_tac 3);
 by (assume_tac 2);
@@ -130,33 +128,24 @@
 by (assume_tac 1);
 by (assume_tac 1);
 by (assume_tac 2);
-by (simp_tac (simpset() addsimps [hastyenv_def]) 1);
+by (asm_simp_tac (simpset() addsimps [hastyenv_def]) 1);
 by (Fast_tac 1);
 qed "consistency_app2";
 
-fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac)); 
-
 Goal "<ve,e,v>:EvalRel ==>         \
 \       (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)";
 by (etac EvalRel.induct 1);
-by (safe_tac ZF_cs);
-by (mt_cases_tac consistency_const);
-by (mt_cases_tac consistency_var);
-by (mt_cases_tac consistency_fn);
-by (mt_cases_tac consistency_fix);
-by (mt_cases_tac consistency_app1);
-by (mt_cases_tac consistency_app2);
+by (blast_tac (claset() addIs [consistency_app2]) 6);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1])));
 qed "consistency";
 
 
-Goal
-  "[| ve:ValEnv; te:TyEnv;              \
-\     isofenv(ve,te);                   \
-\     <ve,e,v_const(c)>:EvalRel;        \
-\     <te,e,t>:ElabRel                  \
-\  |] ==>                               \
-\  isof(c,t)";
-by (rtac (htr_constE) 1);
+Goal "[| ve:ValEnv; te:TyEnv;              \
+\        isofenv(ve,te);                   \
+\        <ve,e,v_const(c)>:EvalRel;        \
+\        <te,e,t>:ElabRel                  \
+\     |] ==> isof(c,t)";
+by (rtac htr_constE 1);
 by (dtac consistency 1);
 by (fast_tac (claset() addSIs [basic_consistency_lem]) 1);
 by (assume_tac 1);

--- a/src/ZF/Coind/Static.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Coind/Static.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -4,27 +4,22 @@
     Copyright   1995  University of Cambridge
 *)
 
-open BCR Static;
+val elab_constE	= ElabRel.mk_cases "<te,e_const(c),t>:ElabRel";
 
-val elab_constE = 
-  ElabRel.mk_cases Exp.con_defs "<te,e_const(c),t>:ElabRel";
+val elab_varE 	= ElabRel.mk_cases "<te,e_var(x),t>:ElabRel";
 
-val elab_varE =
-  ElabRel.mk_cases Exp.con_defs "<te,e_var(x),t>:ElabRel";
+val elab_fnE 	= ElabRel.mk_cases "<te,e_fn(x,e),t>:ElabRel";
 
-val elab_fnE =
-  ElabRel.mk_cases Exp.con_defs "<te,e_fn(x,e),t>:ElabRel";
+val elab_fixE 	= ElabRel.mk_cases "<te,e_fix(f,x,e),t>:ElabRel";
+
+val elab_appE 	= ElabRel.mk_cases "<te,e_app(e1,e2),t>:ElabRel";
 
-val elab_fixE =
-  ElabRel.mk_cases Exp.con_defs "<te,e_fix(f,x,e),t>:ElabRel";
+AddSEs [elab_constE, elab_varE, elab_fixE];
 
-val elab_appE = 
-  ElabRel.mk_cases Exp.con_defs "<te,e_app(e1,e2),t>:ElabRel";
+AddSIs [ElabRel.constI, ElabRel.varI, ElabRel.fnI, ElabRel.fixI];
 
-let open ElabRel in 
-claset_ref() := claset() addSIs [elab_constI,elab_varI,elab_fnI,elab_fixI]
-                  addSEs [elab_constE,elab_varE,elab_fixE]
-		  addIs [elab_appI]
-		  addEs [elab_appE,elab_fnE]
-		  addDs [ElabRel.dom_subset RS subsetD]
-end;
+AddIs  [ElabRel.appI];
+
+AddEs [elab_appE, elab_fnE];
+
+AddDs [ElabRel.dom_subset RS subsetD];

--- a/src/ZF/Coind/Static.thy	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Coind/Static.thy	Tue Jan 19 11:18:11 1999 +0100
@@ -6,26 +6,26 @@
 
 Static = BCR +
 
-consts
-  ElabRel :: i
+consts  ElabRel :: i
+
 inductive
   domains "ElabRel" <= "TyEnv * Exp * Ty"
   intrs
-    elab_constI
+    constI
       " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   
        <te,e_const(c),t>:ElabRel "
-    elab_varI
+    varI
       " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   
        <te,e_var(x),te_app(te,x)>:ElabRel "
-    elab_fnI
+    fnI
       " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   
           <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   
        <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
-    elab_fixI
+    fixI
       " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   
           <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   
        <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
-    elab_appI
+    appI
       " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   
           <te,e1,t_fun(t1,t2)>:ElabRel;   
           <te,e2,t1>:ElabRel |] ==>   

--- a/src/ZF/Coind/Types.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Coind/Types.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -4,10 +4,7 @@
     Copyright   1995  University of Cambridge
 *)
 
-open Types;
-
-val te_owrE = 
-  TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv";
+val te_owrE = TyEnv.mk_cases "te_owr(te,f,t):TyEnv";
 
 Goal "te_app(te_owr(te,x,t),x) = t";
 by (Simp_tac 1);

--- a/src/ZF/Datatype.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Datatype.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -47,3 +47,59 @@
 			  and Ind_Package = CoInd_Package
 			  and Datatype_Arg = CoData_Arg);
 
+
+
+(*Simproc for freeness reasoning: compare datatype constructors for equality*)
+structure DataFree =
+struct
+  (*prove while suppressing timing information*)
+  fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
+
+  val trace = ref false;
+
+  fun mk_new ([],[]) = Const("True",FOLogic.oT)
+    | mk_new (largs,rargs) =
+	fold_bal (app FOLogic.conj) 
+		 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
+
+
+ fun proc sg _ old =
+   let val _ = if !trace then writeln ("data_free: OLD = " ^ 
+				       string_of_cterm (cterm_of sg old))
+	       else ()
+       val (lhs,rhs) = FOLogic.dest_eq old
+       val (lhead, largs) = strip_comb lhs
+       and (rhead, rargs) = strip_comb rhs
+       val lname = #1 (dest_Const lhead)
+       and rname = #1 (dest_Const rhead)
+       val lcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, lname))
+       and rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname))
+       val new = 
+	   if #big_rec_name lcon_info = #big_rec_name rcon_info 
+	       andalso not (null (#free_iffs lcon_info)) then
+	       if lname = rname then mk_new (largs, rargs)
+	       else Const("False",FOLogic.oT)
+	   else raise Match
+       val _ = if !trace then 
+		 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
+	       else ()
+       val ct = Thm.cterm_of sg (Logic.mk_equals (old, new))
+       val thm = prove ct 
+		   (fn _ => [rtac iff_reflection 1,
+			     simp_tac (simpset_of Datatype.thy
+  				          addsimps #free_iffs lcon_info) 1])
+	 handle ERROR =>
+	 error("data_free simproc:\nfailed to prove " ^
+	       string_of_cterm ct)
+   in Some thm end
+   handle _ => None;
+
+
+ val conv = 
+     Simplifier.mk_simproc "data_free"
+       [Thm.read_cterm (sign_of ZF.thy) ("(x::i) = y", FOLogic.oT)]
+       proc;
+end;
+
+
+Addsimprocs [DataFree.conv];

--- a/src/ZF/IMP/Com.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/IMP/Com.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -4,8 +4,6 @@
     Copyright   1994 TUM
 *)
 
-open Com;
-
 val type_cs = claset() addSDs [evala.dom_subset RS subsetD,
 			      evalb.dom_subset RS subsetD,
 			      evalc.dom_subset RS subsetD];
@@ -42,8 +40,8 @@
 
 val aexp_elim_cases = 
    [
-    evala.mk_cases aexp.con_defs "<N(n),sigma> -a-> i",
-    evala.mk_cases aexp.con_defs "<X(x),sigma> -a-> i",
-    evala.mk_cases aexp.con_defs "<Op1(f,e),sigma> -a-> i",
-    evala.mk_cases aexp.con_defs "<Op2(f,a1,a2),sigma>  -a-> i"
+    evala.mk_cases "<N(n),sigma> -a-> i",
+    evala.mk_cases "<X(x),sigma> -a-> i",
+    evala.mk_cases "<Op1(f,e),sigma> -a-> i",
+    evala.mk_cases "<Op2(f,a1,a2),sigma>  -a-> i"
    ];

--- a/src/ZF/IMP/Equiv.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/IMP/Equiv.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -20,12 +20,12 @@
 
 val bexp_elim_cases = 
    [
-    evalb.mk_cases bexp.con_defs "<true,sigma> -b-> x",
-    evalb.mk_cases bexp.con_defs "<false,sigma> -b-> x",
-    evalb.mk_cases bexp.con_defs "<ROp(f,a0,a1),sigma> -b-> x",
-    evalb.mk_cases bexp.con_defs "<noti(b),sigma> -b-> x",
-    evalb.mk_cases bexp.con_defs "<b0 andi b1,sigma> -b-> x",
-    evalb.mk_cases bexp.con_defs "<b0 ori b1,sigma> -b-> x"
+    evalb.mk_cases "<true,sigma> -b-> x",
+    evalb.mk_cases "<false,sigma> -b-> x",
+    evalb.mk_cases "<ROp(f,a0,a1),sigma> -b-> x",
+    evalb.mk_cases "<noti(b),sigma> -b-> x",
+    evalb.mk_cases "<b0 andi b1,sigma> -b-> x",
+    evalb.mk_cases "<b0 ori b1,sigma> -b-> x"
    ];
 
 

--- a/src/ZF/List.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/List.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -9,7 +9,7 @@
 (*** Aspects of the datatype definition ***)
 
 (*An elimination rule, for type-checking*)
-val ConsE = list.mk_cases list.con_defs "Cons(a,l) : list(A)";
+val ConsE = list.mk_cases "Cons(a,l) : list(A)";
 
 (*Proving freeness results*)
 val Cons_iff     = list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";

--- a/src/ZF/Resid/Redex.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Resid/Redex.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -12,10 +12,10 @@
 (*    Specialisation of comp-rules                                           *)
 (* ------------------------------------------------------------------------- *)
 
-val compD1 =Scomp.dom_subset RS subsetD RS SigmaD1;
-val compD2 =Scomp.dom_subset RS subsetD RS SigmaD2;
+val compD1 = Scomp.dom_subset RS subsetD RS SigmaD1;
+val compD2 = Scomp.dom_subset RS subsetD RS SigmaD2;
 
-val regD =Sreg.dom_subset RS subsetD;
+val regD = Sreg.dom_subset RS subsetD;
 
 (* ------------------------------------------------------------------------- *)
 (*    Equality rules for union                                               *)
@@ -29,8 +29,7 @@
 by (asm_simp_tac (simpset() addsimps [union_def]) 1);
 qed "union_Fun";
  
-Goal
- "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
+Goal "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
 \     App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
 by (asm_simp_tac (simpset() addsimps [union_def]) 1);
 qed "union_App";
@@ -42,17 +41,16 @@
 	   union_App,union_Fun,union_Var,compD2,compD1,regD]);
 
 AddIs Scomp.intrs;
-AddSEs [Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))",
-	Sreg.mk_cases redexes.con_defs "regular(Fun(b))",
-	Sreg.mk_cases redexes.con_defs "regular(Var(b))",
-	Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)",
-	Scomp.mk_cases redexes.con_defs "u ~ Fun(t)",
-	Scomp.mk_cases redexes.con_defs "u ~ Var(n)",
-	Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)",
-	Scomp.mk_cases redexes.con_defs "Fun(t) ~ v",
-	Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v",
-	Scomp.mk_cases redexes.con_defs "Var(n) ~ u"
-	];
+AddSEs [Sreg.mk_cases "regular(App(b,f,a))",
+	Sreg.mk_cases "regular(Fun(b))",
+	Sreg.mk_cases "regular(Var(b))",
+	Scomp.mk_cases "Fun(u) ~ Fun(t)",
+	Scomp.mk_cases "u ~ Fun(t)",
+	Scomp.mk_cases "u ~ Var(n)",
+	Scomp.mk_cases "u ~ App(b,t,a)",
+	Scomp.mk_cases "Fun(t) ~ v",
+	Scomp.mk_cases "App(b,f,a) ~ v",
+	Scomp.mk_cases "Var(n) ~ u"];
 
 
 

--- a/src/ZF/Resid/Reduction.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Resid/Reduction.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -5,9 +5,6 @@
     Logic Image: ZF
 *)
 
-open Reduction;
-
-
 (* ------------------------------------------------------------------------- *)
 (*     Setting up rulelists for reduction                                    *)
 (* ------------------------------------------------------------------------- *)
@@ -25,7 +22,7 @@
 AddIs (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
        [Spar_red.one_step, lambda.dom_subset RS subsetD,
 	unmark_type]@lambda.intrs@bool_typechecks);
-AddSEs [Spar_red1.mk_cases redexes.con_defs "Fun(t) =1=> Fun(u)"];
+AddSEs [Spar_red1.mk_cases "Fun(t) =1=> Fun(u)"];
 
 Addsimps (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
 	  [Spar_red.one_step, substL_type, redD1, redD2, par_redD1, 

--- a/src/ZF/Resid/Residuals.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Resid/Residuals.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -10,8 +10,7 @@
 (* ------------------------------------------------------------------------- *)
 
 AddIs (Sres.intrs @ redexes.intrs @ Sreg.intrs @ [subst_type]); 
-AddSEs (redexes.free_SEs @
-	(map (Sres.mk_cases redexes.con_defs) 
+AddSEs (map Sres.mk_cases
 	     ["residuals(Var(n),Var(n),v)",
 	      "residuals(Fun(t),Fun(u),v)",
 	      "residuals(App(b, u1, u2), App(0, v1, v2),v)",
@@ -21,19 +20,21 @@
 	      "residuals(App(b, u1, u2), w,v)",
 	      "residuals(u,Var(n),v)",
 	      "residuals(u,Fun(t),v)",
-	      "residuals(w,App(b, u1, u2),v)"]) @
-	(map (Ssub.mk_cases redexes.con_defs) 
+	      "residuals(w,App(b, u1, u2),v)"]);
+
+AddSEs (map Ssub.mk_cases
 	     ["Var(n) <== u",
 	      "Fun(n) <== u",
 	      "u <== Fun(n)",
 	      "App(1,Fun(t),a) <== u",
-	      "App(0,t,a) <== u"]) @
-	[redexes.mk_cases redexes.con_defs "Fun(t):redexes"]);
+	      "App(0,t,a) <== u"]);
+
+AddSEs [redexes.mk_cases "Fun(t):redexes"];
 
 Addsimps Sres.intrs;
-val resD1 =Sres.dom_subset RS subsetD RS SigmaD1;
-val resD2 =Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1;
-val resD3 =Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2;
+val resD1 = Sres.dom_subset RS subsetD RS SigmaD1;
+val resD2 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1;
+val resD3 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2;
 
 
 (* ------------------------------------------------------------------------- *)
@@ -42,7 +43,7 @@
 
 Goal "residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w";
 by (etac Sres.induct 1);
-by (ALLGOALS Fast_tac);
+by (ALLGOALS Force_tac);
 qed_spec_mp "residuals_function";
 
 Goal "u~v ==> regular(v) --> (EX w. residuals(u,v,w))";
@@ -81,7 +82,8 @@
 Goalw [res_func_def]
     "[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
 \           App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
-by (blast_tac (claset() addSDs [comp_resfuncD]
+by (blast_tac (claset() addSEs redexes.free_SEs
+			addSDs [comp_resfuncD]
 			addIs [residuals_function]) 1);
 qed "res_redex";
 
@@ -98,8 +100,6 @@
 	  lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type,
 	  subst_rec_preserve_reg];
 
-Addsimps redexes.free_iffs;
-
 
 (* ------------------------------------------------------------------------- *)
 (*     Commutation theorem                                                   *)

--- a/src/ZF/Tools/datatype_package.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -380,6 +380,7 @@
         {big_rec_name = big_rec_name,
 	 constructors = constructors,
             (*let primrec handle definition by cases*)
+	 free_iffs = free_iffs,
 	 rec_rewrites = (case recursor_eqns of
 			     [] => case_eqns | _ => recursor_eqns)};
 

--- a/src/ZF/Tools/induct_tacs.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -53,6 +53,7 @@
 type constructor_info =
   {big_rec_name : string,     (*name of the mutually recursive set*)
    constructors : term list,  (*the constructors, as Consts*)
+   free_iffs    : thm list,   (*freeness simprules*)
    rec_rewrites : thm list};  (*recursor equations*)
 
 
@@ -161,6 +162,9 @@
 	  {big_rec_name = big_rec_name,
 	   constructors = constructors,
 	      (*let primrec handle definition by cases*)
+	   free_iffs = [],  (*thus we expect the necessary freeness rewrites
+			      to be in the simpset already, as is the case for
+			      Nat and disjoint sum*)
 	   rec_rewrites = (case recursor_eqns of
 			       [] => case_eqns | _ => recursor_eqns)};
 

--- a/src/ZF/Tools/inductive_package.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -19,7 +19,7 @@
     dom_subset : thm,                  (*inclusion of recursive set in dom*)
     intrs      : thm list,             (*introduction rules*)
     elim       : thm,                  (*case analysis theorem*)
-    mk_cases   : thm list -> string -> thm,    (*generates case theorems*)
+    mk_cases   : string -> thm,        (*generates case theorems*)
     induct     : thm,                  (*main induction rule*)
     mutual_induct : thm};              (*mutual induction rule*)
 
@@ -270,10 +270,10 @@
       the given defs.  Cannot simply use the local con_defs because  
       con_defs=[] for inference systems. 
     String s should have the form t:Si where Si is an inductive set*)
-  fun mk_cases defs s = 
-      rule_by_tactic (rewrite_goals_tac defs THEN 
-		      basic_elim_tac THEN
-		      fold_tac defs)
+  fun mk_cases s = 
+      rule_by_tactic (basic_elim_tac THEN
+		      ALLGOALS Asm_full_simp_tac THEN 
+		      basic_elim_tac)
 	 (assume_read (theory_of_thm elim) s
 	              (*Don't use thy1: it will be stale*)
 	  RS  elim)

--- a/src/ZF/Tools/primrec_package.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -18,10 +18,8 @@
 
 exception RecError of string;
 
-(* FIXME: move? *)
-
-fun dest_eq (Const ("Trueprop", _) $ (Const ("op =", _) $ lhs $ rhs)) = (lhs, rhs)
-  | dest_eq t = raise TERM ("dest_eq", [t])
+(*Remove outer Trueprop and equality sign*)
+val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop;
 
 fun primrec_err s = error ("Primrec definition error:\n" ^ s);
 
@@ -33,9 +31,10 @@
 (*rec_fn_opt records equations already noted for this function*)
 fun process_eqn thy (eq, rec_fn_opt) = 
   let
-    val (lhs, rhs) = if null (term_vars eq) then
-        dest_eq eq handle _ => raise RecError "not a proper equation"
-      else raise RecError "illegal schematic variable(s)";
+    val (lhs, rhs) = 
+	if null (term_vars eq) then
+	    dest_eqn eq handle _ => raise RecError "not a proper equation"
+	else raise RecError "illegal schematic variable(s)";
 
     val (recfun, args) = strip_comb lhs;
     val (fname, ftype) = dest_Const recfun handle _ => 
@@ -104,7 +103,7 @@
       | use_fabs t       = t
 
     val cnames         = map (#1 o dest_Const) constructors
-    and recursor_pairs = map (dest_eq o concl_of) rec_rewrites
+    and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites
 
     fun absterm (Free(a,T), body) = absfree (a,T,body)
       | absterm (t,body)          = Abs("rec", iT, abstract_over (t, body))

--- a/src/ZF/ex/BT.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/ex/BT.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -10,14 +10,14 @@
 
 Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
 by (induct_tac "l" 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs)));
+by (ALLGOALS Asm_full_simp_tac);
 qed_spec_mp "Br_neq_left";
 
 (*Proving a freeness theorem*)
 val Br_iff = bt.mk_free "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'";
 
 (*An elimination rule, for type-checking*)
-val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)";
+val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
 
 (**  Lemmas to justify using "bt" in other recursive type definitions **)
 

--- a/src/ZF/ex/CoUnit.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/ex/CoUnit.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -10,10 +10,8 @@
   Report 334,  Cambridge University Computer Laboratory.  1994.
 *)
 
-open CoUnit;
-  
 (*USELESS because folding on Con(?xa) == ?xa fails*)
-val ConE = counit.mk_cases counit.con_defs "Con(x) : counit";
+val ConE = counit.mk_cases "Con(x) : counit";
 
 (*Proving freeness results*)
 val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y";
@@ -33,7 +31,7 @@
   The resulting set is a singleton.
 *)
 
-val Con2E = counit2.mk_cases counit2.con_defs "Con2(x,y) : counit2";
+val Con2E = counit2.mk_cases "Con2(x,y) : counit2";
 
 (*Proving freeness results*)
 val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";

--- a/src/ZF/ex/Comb.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/ex/Comb.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -15,8 +15,6 @@
 /usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
 *)
 
-open Comb;
-
 (*** Transitive closure preserves the Church-Rosser property ***)
 
 Goalw [diamond_def]
@@ -39,7 +37,7 @@
 
 
 val [_,_,comb_Ap] = comb.intrs;
-val Ap_E = comb.mk_cases comb.con_defs "p#q : comb";
+val Ap_E = comb.mk_cases "p#q : comb";
 
 AddSIs comb.intrs;
 AddSEs comb.free_SEs;
@@ -81,9 +79,9 @@
 (** Non-contraction results **)
 
 (*Derive a case for each combinator constructor*)
-val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
-val S_contractE = contract.mk_cases comb.con_defs "S -1-> r";
-val Ap_contractE = contract.mk_cases comb.con_defs "p#q -1-> r";
+val K_contractE = contract.mk_cases "K -1-> r";
+val S_contractE = contract.mk_cases "S -1-> r";
+val Ap_contractE = contract.mk_cases "p#q -1-> r";
 
 AddIs  [contract.Ap1, contract.Ap2];
 AddSEs [K_contractE, S_contractE, Ap_contractE];
@@ -148,9 +146,9 @@
 qed "field_parcontract_eq";
 
 (*Derive a case for each combinator constructor*)
-val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r";
-val S_parcontractE = parcontract.mk_cases comb.con_defs "S =1=> r";
-val Ap_parcontractE = parcontract.mk_cases comb.con_defs "p#q =1=> r";
+val K_parcontractE = parcontract.mk_cases "K =1=> r";
+val S_parcontractE = parcontract.mk_cases "S =1=> r";
+val Ap_parcontractE = parcontract.mk_cases "p#q =1=> r";
 
 AddIs  parcontract.intrs;
 AddSEs [Ap_E, K_parcontractE, S_parcontractE, Ap_parcontractE];

--- a/src/ZF/ex/Enum.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/ex/Enum.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -8,9 +8,7 @@
 Can go up to at least 100 constructors, but it takes nearly 7 minutes...
 *)
 
-open Enum;
-
 Goal "C00 ~= C01";
-by (simp_tac (simpset() addsimps enum.free_iffs) 1);
+by (Simp_tac 1);
 result();
 

--- a/src/ZF/ex/LList.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/ex/LList.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -6,8 +6,9 @@
 Codatatype definition of Lazy Lists
 *)
 
-open LList;
-
+(*These commands cause classical reasoning to regard the subset relation
+  as primitive, not reducing it to membership*)
+  
 Delrules [subsetI, subsetCE];
 AddSIs [subset_refl, cons_subsetI, subset_consI, 
 	Union_least, UN_least, Un_least, 
@@ -15,7 +16,7 @@
 	Un_upper1, Un_upper2, Int_lower1, Int_lower2];
 
 (*An elimination rule, for type-checking*)
-val LConsE = llist.mk_cases llist.con_defs "LCons(a,l) : llist(A)";
+val LConsE = llist.mk_cases "LCons(a,l) : llist(A)";
 
 (*Proving freeness results*)
 val LCons_iff      = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";

--- a/src/ZF/ex/ListN.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/ex/ListN.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -9,8 +9,6 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-open ListN;
-
 Goal "l:list(A) ==> <length(l),l> : listn(A)";
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
@@ -40,8 +38,8 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs)));
 qed "listn_append";
 
-val Nil_listn_case = listn.mk_cases list.con_defs "<i,Nil> : listn(A)"
-and Cons_listn_case = listn.mk_cases list.con_defs "<i,Cons(x,l)> : listn(A)";
+val Nil_listn_case  = listn.mk_cases "<i,Nil> : listn(A)"
+and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> : listn(A)";
 
-val zero_listn_case = listn.mk_cases list.con_defs "<0,l> : listn(A)"
-and succ_listn_case = listn.mk_cases list.con_defs "<succ(i),l> : listn(A)";
+val zero_listn_case = listn.mk_cases "<0,l> : listn(A)"
+and succ_listn_case = listn.mk_cases "<succ(i),l> : listn(A)";

--- a/src/ZF/ex/PropLog.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/ex/PropLog.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -40,7 +40,7 @@
 
 val thms_in_pl = thms.dom_subset RS subsetD;
 
-val ImpE = prop.mk_cases prop.con_defs "p=>q : prop";
+val ImpE = prop.mk_cases "p=>q : prop";
 
 (*Stronger Modus Ponens rule: no typechecking!*)
 Goal "[| H |- p=>q;  H |- p |] ==> H |- q";
@@ -166,22 +166,14 @@
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
 Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
 by (etac prop.induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addSEs prop.free_SEs) 1);
-by (Asm_simp_tac 1);
-by (Fast_tac 1);
+by Auto_tac;
 qed "hyps_Diff";
 
 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
   we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
 Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
 by (etac prop.induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addSEs prop.free_SEs) 1);
-by (Asm_simp_tac 1);
-by (Fast_tac 1);
+by Auto_tac;
 qed "hyps_cons";
 
 (** Two lemmas for use with weaken_left **)

--- a/src/ZF/ex/Rmap.ML	Tue Jan 19 11:16:39 1999 +0100
+++ b/src/ZF/ex/Rmap.ML	Tue Jan 19 11:18:11 1999 +0100
@@ -6,8 +6,6 @@
 Inductive definition of an operator to "map" a relation over a list
 *)
 
-open Rmap;
-
 Goalw rmap.defs "r<=s ==> rmap(r) <= rmap(s)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac rmap.bnd_mono 1));
@@ -15,8 +13,8 @@
                       basic_monos) 1));
 qed "rmap_mono";
 
-val Nil_rmap_case = rmap.mk_cases list.con_defs "<Nil,zs> : rmap(r)"
-and Cons_rmap_case = rmap.mk_cases list.con_defs "<Cons(x,xs),zs> : rmap(r)";
+val Nil_rmap_case  = rmap.mk_cases "<Nil,zs> : rmap(r)"
+and Cons_rmap_case = rmap.mk_cases "<Cons(x,xs),zs> : rmap(r)";
 
 AddIs  rmap.intrs;
 AddSEs [Nil_rmap_case, Cons_rmap_case];
@@ -43,16 +41,16 @@
 (** If f is a function then rmap(f) behaves as expected. **)
 
 Goal "f: A->B ==> rmap(f): list(A)->list(B)";
-by (asm_full_simp_tac 
-    (simpset() addsimps [Pi_iff, rmap_rel_type, rmap_functional, rmap_total]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Pi_iff, rmap_rel_type,
+					   rmap_functional, rmap_total]) 1);
 qed "rmap_fun_type";
 
 Goalw [apply_def] "rmap(f)`Nil = Nil";
 by (Blast_tac 1);
 qed "rmap_Nil";
 
-Goal "[| f: A->B;  x: A;  xs: list(A) |] ==> \
-\                   rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
+Goal "[| f: A->B;  x: A;  xs: list(A) |]  \
+\     ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
 by (rtac apply_equality 1);
 by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
 qed "rmap_Cons";