removed legacy ML bindings;
authorwenzelm
Wed Dec 06 01:12:36 2006 +0100 (2006-12-06)
changeset 21669c68717c16013
parent 21668 2d811ae6752a
child 21670 704510b508ef
removed legacy ML bindings;
src/HOL/Bali/AxCompl.thy
src/HOL/Datatype.ML
src/HOL/Datatype.thy
src/HOL/Finite_Set.ML
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/HoareParallel/Mul_Gar_Coll.thy
src/HOL/IsaMakefile
src/HOL/Lambda/Commutation.thy
src/HOL/List.ML
src/HOL/Nat.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Orderings.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Set.thy
src/HOL/Transitive_Closure.ML
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/W0/W0.thy
src/HOL/ex/MT.ML
src/HOL/ex/reflection.ML
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Wed Dec 06 01:12:36 2006 +0100
     1.3 @@ -1406,7 +1406,7 @@
     1.4  apply -
     1.5  apply (induct_tac "n")
     1.6  apply  (tactic "ALLGOALS Clarsimp_tac")
     1.7 -apply  (tactic "dtac (permute_prems 0 1 card_seteq) 1")
     1.8 +apply  (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *})
     1.9  apply    simp
    1.10  apply   (erule finite_imageI)
    1.11  apply  (simp add: MGF_asm ax_derivs_asm)
     2.1 --- a/src/HOL/Datatype.ML	Tue Dec 05 22:14:53 2006 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,91 +0,0 @@
     2.4 -(*  Title:      HOL/Datatype.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     2.7 -*)
     2.8 -
     2.9 -(** legacy ML bindings **)
    2.10 -
    2.11 -structure bool =
    2.12 -struct
    2.13 -  val distinct = thms "bool.distinct";
    2.14 -  val inject = thms "bool.inject";
    2.15 -  val exhaust = thm "bool.exhaust";
    2.16 -  val cases = thms "bool.cases";
    2.17 -  val split = thm "bool.split";
    2.18 -  val split_asm = thm "bool.split_asm";
    2.19 -  val induct = thm "bool.induct";
    2.20 -  val recs = thms "bool.recs";
    2.21 -  val simps = thms "bool.simps";
    2.22 -  val size = thms "bool.size";
    2.23 -end;
    2.24 -
    2.25 -structure sum =
    2.26 -struct
    2.27 -  val distinct = thms "sum.distinct";
    2.28 -  val inject = thms "sum.inject";
    2.29 -  val exhaust = thm "sum.exhaust";
    2.30 -  val cases = thms "sum.cases";
    2.31 -  val split = thm "sum.split";
    2.32 -  val split_asm = thm "sum.split_asm";
    2.33 -  val induct = thm "sum.induct";
    2.34 -  val recs = thms "sum.recs";
    2.35 -  val simps = thms "sum.simps";
    2.36 -  val size = thms "sum.size";
    2.37 -end;
    2.38 -
    2.39 -structure unit =
    2.40 -struct
    2.41 -  val distinct = thms "unit.distinct";
    2.42 -  val inject = thms "unit.inject";
    2.43 -  val exhaust = thm "unit.exhaust";
    2.44 -  val cases = thms "unit.cases";
    2.45 -  val split = thm "unit.split";
    2.46 -  val split_asm = thm "unit.split_asm";
    2.47 -  val induct = thm "unit.induct";
    2.48 -  val recs = thms "unit.recs";
    2.49 -  val simps = thms "unit.simps";
    2.50 -  val size = thms "unit.size";
    2.51 -end;
    2.52 -
    2.53 -structure prod =
    2.54 -struct
    2.55 -  val distinct = thms "prod.distinct";
    2.56 -  val inject = thms "prod.inject";
    2.57 -  val exhaust = thm "prod.exhaust";
    2.58 -  val cases = thms "prod.cases";
    2.59 -  val split = thm "prod.split";
    2.60 -  val split_asm = thm "prod.split_asm";
    2.61 -  val induct = thm "prod.induct";
    2.62 -  val recs = thms "prod.recs";
    2.63 -  val simps = thms "prod.simps";
    2.64 -  val size = thms "prod.size";
    2.65 -end;
    2.66 -
    2.67 -structure option =
    2.68 -struct
    2.69 -  val distinct = thms "option.distinct";
    2.70 -  val inject = thms "option.inject";
    2.71 -  val exhaust = thm "option.exhaust";
    2.72 -  val cases = thms "option.cases";
    2.73 -  val split = thm "option.split";
    2.74 -  val split_asm = thm "option.split_asm";
    2.75 -  val induct = thm "option.induct";
    2.76 -  val recs = thms "option.recs";
    2.77 -  val simps = thms "option.simps";
    2.78 -  val size = thms "option.size";
    2.79 -end;
    2.80 -
    2.81 -val elem_o2s = thm "elem_o2s";
    2.82 -val not_None_eq = thm "not_None_eq";
    2.83 -val not_Some_eq = thm "not_Some_eq";
    2.84 -val o2s_empty_eq = thm "o2s_empty_eq";
    2.85 -val option_caseE = thm "option_caseE";
    2.86 -val option_map_None = thm "option_map_None";
    2.87 -val option_map_Some = thm "option_map_Some";
    2.88 -val option_map_def = thm "option_map_def";
    2.89 -val option_map_eq_Some = thm "option_map_eq_Some";
    2.90 -val option_map_o_sum_case = thm "option_map_o_sum_case";
    2.91 -val ospec = thm "ospec";
    2.92 -val sum_case_inject = thm "sum_case_inject";
    2.93 -val sum_case_weak_cong = thm "sum_case_weak_cong";
    2.94 -val surjective_sum = thm "surjective_sum";
     3.1 --- a/src/HOL/Datatype.thy	Tue Dec 05 22:14:53 2006 +0100
     3.2 +++ b/src/HOL/Datatype.thy	Wed Dec 06 01:12:36 2006 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  Could <*> be generalized to a general summation (Sigma)?
     3.5  *)
     3.6  
     3.7 -header{*Analogues of the Cartesian Product and Disjoint Sum for Datatypes*}
     3.8 +header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     3.9  
    3.10  theory Datatype
    3.11  imports Nat Sum_Type
    3.12 @@ -808,95 +808,12 @@
    3.13  code_reserved Haskell
    3.14    Bool True False not Maybe Nothing Just
    3.15  
    3.16 -ML
    3.17 -{*
    3.18 -val apfst_conv = thm "apfst_conv";
    3.19 -val apfst_convE = thm "apfst_convE";
    3.20 -val Push_inject1 = thm "Push_inject1";
    3.21 -val Push_inject2 = thm "Push_inject2";
    3.22 -val Push_inject = thm "Push_inject";
    3.23 -val Push_neq_K0 = thm "Push_neq_K0";
    3.24 -val Abs_Node_inj = thm "Abs_Node_inj";
    3.25 -val Node_K0_I = thm "Node_K0_I";
    3.26 -val Node_Push_I = thm "Node_Push_I";
    3.27 -val Scons_not_Atom = thm "Scons_not_Atom";
    3.28 -val Atom_not_Scons = thm "Atom_not_Scons";
    3.29 -val inj_Atom = thm "inj_Atom";
    3.30 -val Atom_inject = thm "Atom_inject";
    3.31 -val Atom_Atom_eq = thm "Atom_Atom_eq";
    3.32 -val inj_Leaf = thm "inj_Leaf";
    3.33 -val Leaf_inject = thm "Leaf_inject";
    3.34 -val inj_Numb = thm "inj_Numb";
    3.35 -val Numb_inject = thm "Numb_inject";
    3.36 -val Push_Node_inject = thm "Push_Node_inject";
    3.37 -val Scons_inject1 = thm "Scons_inject1";
    3.38 -val Scons_inject2 = thm "Scons_inject2";
    3.39 -val Scons_inject = thm "Scons_inject";
    3.40 -val Scons_Scons_eq = thm "Scons_Scons_eq";
    3.41 -val Scons_not_Leaf = thm "Scons_not_Leaf";
    3.42 -val Leaf_not_Scons = thm "Leaf_not_Scons";
    3.43 -val Scons_not_Numb = thm "Scons_not_Numb";
    3.44 -val Numb_not_Scons = thm "Numb_not_Scons";
    3.45 -val Leaf_not_Numb = thm "Leaf_not_Numb";
    3.46 -val Numb_not_Leaf = thm "Numb_not_Leaf";
    3.47 -val ndepth_K0 = thm "ndepth_K0";
    3.48 -val ndepth_Push_Node_aux = thm "ndepth_Push_Node_aux";
    3.49 -val ndepth_Push_Node = thm "ndepth_Push_Node";
    3.50 -val ntrunc_0 = thm "ntrunc_0";
    3.51 -val ntrunc_Atom = thm "ntrunc_Atom";
    3.52 -val ntrunc_Leaf = thm "ntrunc_Leaf";
    3.53 -val ntrunc_Numb = thm "ntrunc_Numb";
    3.54 -val ntrunc_Scons = thm "ntrunc_Scons";
    3.55 -val ntrunc_one_In0 = thm "ntrunc_one_In0";
    3.56 -val ntrunc_In0 = thm "ntrunc_In0";
    3.57 -val ntrunc_one_In1 = thm "ntrunc_one_In1";
    3.58 -val ntrunc_In1 = thm "ntrunc_In1";
    3.59 -val uprodI = thm "uprodI";
    3.60 -val uprodE = thm "uprodE";
    3.61 -val uprodE2 = thm "uprodE2";
    3.62 -val usum_In0I = thm "usum_In0I";
    3.63 -val usum_In1I = thm "usum_In1I";
    3.64 -val usumE = thm "usumE";
    3.65 -val In0_not_In1 = thm "In0_not_In1";
    3.66 -val In1_not_In0 = thm "In1_not_In0";
    3.67 -val In0_inject = thm "In0_inject";
    3.68 -val In1_inject = thm "In1_inject";
    3.69 -val In0_eq = thm "In0_eq";
    3.70 -val In1_eq = thm "In1_eq";
    3.71 -val inj_In0 = thm "inj_In0";
    3.72 -val inj_In1 = thm "inj_In1";
    3.73 -val Lim_inject = thm "Lim_inject";
    3.74 -val ntrunc_subsetI = thm "ntrunc_subsetI";
    3.75 -val ntrunc_subsetD = thm "ntrunc_subsetD";
    3.76 -val ntrunc_equality = thm "ntrunc_equality";
    3.77 -val ntrunc_o_equality = thm "ntrunc_o_equality";
    3.78 -val uprod_mono = thm "uprod_mono";
    3.79 -val usum_mono = thm "usum_mono";
    3.80 -val Scons_mono = thm "Scons_mono";
    3.81 -val In0_mono = thm "In0_mono";
    3.82 -val In1_mono = thm "In1_mono";
    3.83 -val Split = thm "Split";
    3.84 -val Case_In0 = thm "Case_In0";
    3.85 -val Case_In1 = thm "Case_In1";
    3.86 -val ntrunc_UN1 = thm "ntrunc_UN1";
    3.87 -val Scons_UN1_x = thm "Scons_UN1_x";
    3.88 -val Scons_UN1_y = thm "Scons_UN1_y";
    3.89 -val In0_UN1 = thm "In0_UN1";
    3.90 -val In1_UN1 = thm "In1_UN1";
    3.91 -val dprodI = thm "dprodI";
    3.92 -val dprodE = thm "dprodE";
    3.93 -val dsum_In0I = thm "dsum_In0I";
    3.94 -val dsum_In1I = thm "dsum_In1I";
    3.95 -val dsumE = thm "dsumE";
    3.96 -val dprod_mono = thm "dprod_mono";
    3.97 -val dsum_mono = thm "dsum_mono";
    3.98 -val dprod_Sigma = thm "dprod_Sigma";
    3.99 -val dprod_subset_Sigma = thm "dprod_subset_Sigma";
   3.100 -val dprod_subset_Sigma2 = thm "dprod_subset_Sigma2";
   3.101 -val dsum_Sigma = thm "dsum_Sigma";
   3.102 -val dsum_subset_Sigma = thm "dsum_subset_Sigma";
   3.103 -val Domain_dprod = thm "Domain_dprod";
   3.104 -val Domain_dsum = thm "Domain_dsum";
   3.105 +
   3.106 +subsection {* Basic ML bindings *}
   3.107 +
   3.108 +ML {*
   3.109 +val not_None_eq = thm "not_None_eq";
   3.110 +val not_Some_eq = thm "not_Some_eq";
   3.111  *}
   3.112  
   3.113  end
     4.1 --- a/src/HOL/Finite_Set.ML	Tue Dec 05 22:14:53 2006 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,102 +0,0 @@
     4.4 -
     4.5 -(* legacy ML bindings *)
     4.6 -
     4.7 -structure Finites =
     4.8 -struct
     4.9 -  val intrs = thms "Finites.intros";
    4.10 -  val elims = thms "Finites.cases";
    4.11 -  val elim = thm "Finites.cases";
    4.12 -  val induct = thm "Finites.induct";
    4.13 -  val mk_cases = OldInductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
    4.14 -  val [emptyI, insertI] = thms "Finites.intros";
    4.15 -end;
    4.16 -
    4.17 -structure foldSet =
    4.18 -struct
    4.19 -  val intrs = thms "foldSet.intros";
    4.20 -  val elims = thms "foldSet.cases";
    4.21 -  val elim = thm "foldSet.cases";
    4.22 -  val induct = thm "foldSet.induct";
    4.23 -  val mk_cases = OldInductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
    4.24 -  val [emptyI, insertI] = thms "foldSet.intros";
    4.25 -end;
    4.26 -
    4.27 -val card_0_eq = thm "card_0_eq";
    4.28 -val card_Diff1_le = thm "card_Diff1_le";
    4.29 -val card_Diff1_less = thm "card_Diff1_less";
    4.30 -val card_Diff2_less = thm "card_Diff2_less";
    4.31 -val card_Diff_singleton = thm "card_Diff_singleton";
    4.32 -val card_Diff_singleton_if = thm "card_Diff_singleton_if";
    4.33 -val card_Diff_subset = thm "card_Diff_subset";
    4.34 -val card_Pow = thm "card_Pow";
    4.35 -val card_Suc_Diff1 = thm "card_Suc_Diff1";
    4.36 -val card_Un_Int = thm "card_Un_Int";
    4.37 -val card_Un_disjoint = thm "card_Un_disjoint";
    4.38 -val card_bij_eq = thm "card_bij_eq";
    4.39 -val card_def = thm "card_def";
    4.40 -val card_empty = thm "card_empty";
    4.41 -val card_eq_setsum = thm "card_eq_setsum";
    4.42 -val card_image = thm "card_image";
    4.43 -val card_image_le = thm "card_image_le";
    4.44 -val card_inj_on_le = thm "card_inj_on_le";
    4.45 -val card_insert = thm "card_insert";
    4.46 -val card_insert_disjoint = thm "card_insert_disjoint";
    4.47 -val card_insert_if = thm "card_insert_if";
    4.48 -val card_insert_le = thm "card_insert_le";
    4.49 -val card_mono = thm "card_mono";
    4.50 -val card_psubset = thm "card_psubset";
    4.51 -val card_seteq = thm "card_seteq";
    4.52 -val Diff1_foldSet = thm "Diff1_foldSet";
    4.53 -val dvd_partition = thm "dvd_partition";
    4.54 -val empty_foldSetE = thm "empty_foldSetE";
    4.55 -val endo_inj_surj = thm "endo_inj_surj";
    4.56 -val finite = thm "finite";
    4.57 -val finite_Diff = thm "finite_Diff";
    4.58 -val finite_Diff_insert = thm "finite_Diff_insert";
    4.59 -val finite_Field = thm "finite_Field";
    4.60 -val finite_imp_foldSet = thm "finite_imp_foldSet";
    4.61 -val finite_Int = thm "finite_Int";
    4.62 -val finite_Pow_iff = thm "finite_Pow_iff";
    4.63 -val finite_Prod_UNIV = thm "finite_Prod_UNIV";
    4.64 -val finite_SigmaI = thm "finite_SigmaI";
    4.65 -val finite_UN = thm "finite_UN";
    4.66 -val finite_UN_I = thm "finite_UN_I";
    4.67 -val finite_Un = thm "finite_Un";
    4.68 -val finite_UnI = thm "finite_UnI";
    4.69 -val finite_converse = thm "finite_converse";
    4.70 -val finite_empty_induct = thm "finite_empty_induct";
    4.71 -val finite_imageD = thm "finite_imageD";
    4.72 -val finite_imageI = thm "finite_imageI";
    4.73 -val finite_induct = thm "finite_induct";
    4.74 -val finite_insert = thm "finite_insert";
    4.75 -val finite_range_imageI = thm "finite_range_imageI";
    4.76 -val finite_subset = thm "finite_subset";
    4.77 -val finite_subset_induct = thm "finite_subset_induct";
    4.78 -val finite_trancl = thm "finite_trancl";
    4.79 -val foldSet_determ = thm "ACf.foldSet_determ";
    4.80 -val foldSet_imp_finite = thm "foldSet_imp_finite";
    4.81 -val fold_Un_Int = thm "ACe.fold_Un_Int";
    4.82 -val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
    4.83 -val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint";
    4.84 -val fold_commute = thm "ACf.fold_commute";
    4.85 -val fold_def = thm "fold_def";
    4.86 -val fold_empty = thm "fold_empty";
    4.87 -val fold_equality = thm "ACf.fold_equality";
    4.88 -val fold_insert = thm "ACf.fold_insert";
    4.89 -val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int";
    4.90 -val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint";
    4.91 -val psubset_card_mono = thm "psubset_card_mono";
    4.92 -val setsum_0 = thm "setsum_0";
    4.93 -val setsum_SucD = thm "setsum_SucD";
    4.94 -val setsum_UN_disjoint = thm "setsum_UN_disjoint";
    4.95 -val setsum_Un = thm "setsum_Un";
    4.96 -val setsum_Un_Int = thm "setsum_Un_Int";
    4.97 -val setsum_Un_disjoint = thm "setsum_Un_disjoint";
    4.98 -val setsum_addf = thm "setsum_addf";
    4.99 -val setsum_cong = thm "setsum_cong";
   4.100 -val setsum_def = thm "setsum_def";
   4.101 -val setsum_diff1 = thm "setsum_diff1";
   4.102 -val setsum_empty = thm "setsum_empty";
   4.103 -val setsum_eq_0_iff = thm "setsum_eq_0_iff";
   4.104 -val setsum_insert = thm "setsum_insert";
   4.105 -val trancl_subset_Field2 = thm "trancl_subset_Field2";
     5.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Tue Dec 05 22:14:53 2006 +0100
     5.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Wed Dec 06 01:12:36 2006 +0100
     5.3 @@ -798,7 +798,7 @@
     5.4  apply simp_all
     5.5  apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
     5.6  apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
     5.7 -apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
     5.8 +apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
     5.9  done
    5.10  
    5.11  subsubsection {* Interference freedom Mutator-Collector *}
     6.1 --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Tue Dec 05 22:14:53 2006 +0100
     6.2 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Dec 06 01:12:36 2006 +0100
     6.3 @@ -1211,15 +1211,15 @@
     6.4  apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
     6.5  apply(simp_all add:Graph10)
     6.6  --{* 47 subgoals left *}
     6.7 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
     6.8 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
     6.9  --{* 41 subgoals left *}
    6.10  apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
    6.11  --{* 35 subgoals left *}
    6.12 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
    6.13 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
    6.14  --{* 31 subgoals left *}
    6.15 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
    6.16 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
    6.17  --{* 29 subgoals left *}
    6.18 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
    6.19 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
    6.20  --{* 25 subgoals left *}
    6.21  apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
    6.22  --{* 10 subgoals left *}
     7.1 --- a/src/HOL/IsaMakefile	Tue Dec 05 22:14:53 2006 +0100
     7.2 +++ b/src/HOL/IsaMakefile	Wed Dec 06 01:12:36 2006 +0100
     7.3 @@ -84,9 +84,8 @@
     7.4    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML			\
     7.5    $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML			\
     7.6    Tools/res_atpset.ML \
     7.7 -  Code_Generator.thy Datatype.ML Datatype.thy			\
     7.8 -  Divides.thy						\
     7.9 -  Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy		\
    7.10 +  Code_Generator.thy Datatype.thy Divides.thy					\
    7.11 +  Equiv_Relations.thy Extraction.thy Finite_Set.thy				\
    7.12    FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy	\
    7.13    Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy				\
    7.14    Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy			\
    7.15 @@ -94,11 +93,10 @@
    7.16    Integ/cooper_proof.ML Integ/reflected_presburger.ML				\
    7.17    Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML	\
    7.18    Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy		\
    7.19 -  Lattices.thy List.ML List.thy Main.thy Map.thy			\
    7.20 -  Nat.ML Nat.thy OrderedGroup.ML OrderedGroup.thy	\
    7.21 -  Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
    7.22 +  Lattices.thy List.thy Main.thy Map.thy Nat.thy Nat.ML OrderedGroup.ML		\
    7.23 +  OrderedGroup.thy Orderings.thy Power.thy PreList.thy Product_Type.thy		\
    7.24    ROOT.ML Recdef.thy Record.thy Refute.thy			\
    7.25 -  Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML		\
    7.26 +  Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy 			\
    7.27    Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
    7.28    Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML 					\
    7.29    Tools/cnf_funcs.ML					\
    7.30 @@ -117,9 +115,8 @@
    7.31    Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
    7.32    Tools/typecopy_package.ML	\
    7.33    Tools/typedef_package.ML Tools/typedef_codegen.ML	\
    7.34 -  Transitive_Closure.ML Transitive_Closure.thy		\
    7.35 -  Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
    7.36 -  arith_data.ML			\
    7.37 +  Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy		\
    7.38 +  Wellfounded_Relations.thy arith_data.ML			\
    7.39    document/root.tex hologic.ML simpdata.ML ATP_Linkup.thy \
    7.40    Tools/res_atp_provers.ML Tools/res_atp_methods.ML	\
    7.41    Tools/res_hol_clause.ML	\
     8.1 --- a/src/HOL/Lambda/Commutation.thy	Tue Dec 05 22:14:53 2006 +0100
     8.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Dec 06 01:12:36 2006 +0100
     8.3 @@ -130,8 +130,9 @@
     8.4    apply (tactic {* safe_tac HOL_cs *})
     8.5     apply (tactic {*
     8.6       blast_tac (HOL_cs addIs
     8.7 -       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
     8.8 -       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
     8.9 +       [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans",
    8.10 +        thm "rtrancl_converseI", thm "converseI",
    8.11 +        thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *})
    8.12    apply (erule rtrancl_induct)
    8.13     apply blast
    8.14    apply (blast del: rtrancl_refl intro: rtrancl_trans)
     9.1 --- a/src/HOL/List.ML	Tue Dec 05 22:14:53 2006 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,231 +0,0 @@
     9.4 -
     9.5 -(** legacy ML bindings **)
     9.6 -
     9.7 -val Cons_eq_appendI = thm "Cons_eq_appendI";
     9.8 -val Cons_in_lex = thm "Cons_in_lex";
     9.9 -val Nil2_notin_lex = thm "Nil2_notin_lex";
    9.10 -val Nil_eq_concat_conv = thm "Nil_eq_concat_conv";
    9.11 -val Nil_is_append_conv = thm "Nil_is_append_conv";
    9.12 -val Nil_is_map_conv = thm "Nil_is_map_conv";
    9.13 -val Nil_is_rev_conv = thm "Nil_is_rev_conv";
    9.14 -val Nil_notin_lex = thm "Nil_notin_lex";
    9.15 -val all_nth_imp_all_set = thm "all_nth_imp_all_set";
    9.16 -val all_set_conv_all_nth = thm "all_set_conv_all_nth";
    9.17 -val append1_eq_conv = thm "append1_eq_conv";
    9.18 -val append_Cons = thm "append_Cons";
    9.19 -val append_Nil = thm "append_Nil";
    9.20 -val append_Nil2 = thm "append_Nil2";
    9.21 -val append_assoc = thm "append_assoc";
    9.22 -val append_butlast_last_id = thm "append_butlast_last_id";
    9.23 -val append_eq_appendI = thm "append_eq_appendI";
    9.24 -val append_eq_append_conv = thm "append_eq_append_conv";
    9.25 -val append_eq_conv_conj = thm "append_eq_conv_conj";
    9.26 -val append_in_lists_conv = thm "append_in_lists_conv";
    9.27 -val append_is_Nil_conv = thm "append_is_Nil_conv";
    9.28 -val append_same_eq = thm "append_same_eq";
    9.29 -val append_self_conv = thm "append_self_conv";
    9.30 -val append_self_conv2 = thm "append_self_conv2";
    9.31 -val append_take_drop_id = thm "append_take_drop_id";
    9.32 -val butlast_append = thm "butlast_append";
    9.33 -val butlast_snoc = thm "butlast_snoc";
    9.34 -val concat_append = thm "concat_append";
    9.35 -val concat_eq_Nil_conv = thm "concat_eq_Nil_conv";
    9.36 -val distinct_append = thm "distinct_append";
    9.37 -val distinct_filter = thm "distinct_filter";
    9.38 -val distinct_remdups = thm "distinct_remdups";
    9.39 -val dropWhile_append1 = thm "dropWhile_append1";
    9.40 -val dropWhile_append2 = thm "dropWhile_append2";
    9.41 -val drop_0 = thm "drop_0";
    9.42 -val drop_Cons = thm "drop_Cons";
    9.43 -val drop_Cons' = thm "drop_Cons'";
    9.44 -val drop_Nil = thm "drop_Nil";
    9.45 -val drop_Suc_Cons = thm "drop_Suc_Cons";
    9.46 -val drop_all = thm "drop_all";
    9.47 -val drop_append = thm "drop_append";
    9.48 -val drop_drop = thm "drop_drop";
    9.49 -val drop_map = thm "drop_map";
    9.50 -val elem_le_sum = thm "elem_le_sum";
    9.51 -val eq_Nil_appendI = thm "eq_Nil_appendI";
    9.52 -val filter_False = thm "filter_False";
    9.53 -val filter_True = thm "filter_True";
    9.54 -val filter_append = thm "filter_append";
    9.55 -val filter_concat = thm "filter_concat"; 
    9.56 -val filter_filter = thm "filter_filter";
    9.57 -val filter_is_subset = thm "filter_is_subset";
    9.58 -val finite_set = thm "finite_set";
    9.59 -val foldl_Cons = thm "foldl_Cons";
    9.60 -val foldl_Nil = thm "foldl_Nil";
    9.61 -val foldl_append = thm "foldl_append";
    9.62 -val hd_Cons_tl = thm "hd_Cons_tl";
    9.63 -val hd_append = thm "hd_append";
    9.64 -val hd_append2 = thm "hd_append2";
    9.65 -val hd_replicate = thm "hd_replicate";
    9.66 -val in_listsD = thm "in_listsD";
    9.67 -val in_listsI = thm "in_listsI";
    9.68 -val in_lists_conv_set = thm "in_lists_conv_set";
    9.69 -val in_set_butlastD = thm "in_set_butlastD";
    9.70 -val in_set_butlast_appendI = thm "in_set_butlast_appendI";
    9.71 -val in_set_conv_decomp = thm "in_set_conv_decomp";
    9.72 -val in_set_replicateD = thm "in_set_replicateD";
    9.73 -val inj_map = thm "inj_map";
    9.74 -val inj_mapD = thm "inj_mapD";
    9.75 -val inj_mapI = thm "inj_mapI";
    9.76 -val last_replicate = thm "last_replicate";
    9.77 -val last_snoc = thm "last_snoc";
    9.78 -val length_0_conv = thm "length_0_conv";
    9.79 -val length_Suc_conv = thm "length_Suc_conv";
    9.80 -val length_append = thm "length_append";
    9.81 -val length_butlast = thm "length_butlast";
    9.82 -val length_drop = thm "length_drop";
    9.83 -val length_filter_le = thm "length_filter_le";
    9.84 -val length_greater_0_conv = thm "length_greater_0_conv";
    9.85 -val length_induct = thm "length_induct";
    9.86 -val length_list_update = thm "length_list_update";
    9.87 -val length_map = thm "length_map";
    9.88 -val length_replicate = thm "length_replicate";
    9.89 -val length_rev = thm "length_rev";
    9.90 -val length_take = thm "length_take";
    9.91 -val length_tl = thm "length_tl";
    9.92 -val length_upt = thm "length_upt";
    9.93 -val length_zip = thm "length_zip";
    9.94 -val lex_conv = thm "lex_conv";
    9.95 -val lex_def = thm "lex_def";
    9.96 -val lenlex_conv = thm "lenlex_conv";
    9.97 -val lenlex_def = thm "lenlex_def";
    9.98 -val lexn_conv = thm "lexn_conv";
    9.99 -val lexn_length = thm "lexn_length";
   9.100 -val list_all2_Cons = thm "list_all2_Cons";
   9.101 -val list_all2_Cons1 = thm "list_all2_Cons1";
   9.102 -val list_all2_Cons2 = thm "list_all2_Cons2";
   9.103 -val list_all2_Nil = thm "list_all2_Nil";
   9.104 -val list_all2_Nil2 = thm "list_all2_Nil2";
   9.105 -val list_all2_append1 = thm "list_all2_append1";
   9.106 -val list_all2_append2 = thm "list_all2_append2";
   9.107 -val list_all2_conv_all_nth = thm "list_all2_conv_all_nth";
   9.108 -val list_all2_def = thm "list_all2_def";
   9.109 -val list_all2_lengthD = thm "list_all2_lengthD";
   9.110 -val list_all2_rev = thm "list_all2_rev";
   9.111 -val list_all2_trans = thm "list_all2_trans";
   9.112 -val list_all_append = thm "list_all_append";
   9.113 -val list_all_iff = thm "list_all_iff";
   9.114 -val list_ball_nth = thm "list_ball_nth";
   9.115 -val list_update_overwrite = thm "list_update_overwrite";
   9.116 -val list_update_same_conv = thm "list_update_same_conv";
   9.117 -val listsE = thm "listsE";
   9.118 -val lists_IntI = thm "lists_IntI";
   9.119 -val lists_Int_eq = thm "lists_Int_eq";
   9.120 -val lists_mono = thm "lists_mono";
   9.121 -val map_Suc_upt = thm "map_Suc_upt";
   9.122 -val map_append = thm "map_append";
   9.123 -val map_compose = thm "map_compose";
   9.124 -val map_concat = thm "map_concat";
   9.125 -val map_cong = thm "map_cong";
   9.126 -val map_eq_Cons_conv = thm "map_eq_Cons_conv";
   9.127 -val map_ext = thm "map_ext";
   9.128 -val map_ident = thm "map_ident";
   9.129 -val map_injective = thm "map_injective";
   9.130 -val map_is_Nil_conv = thm "map_is_Nil_conv";
   9.131 -val map_replicate = thm "map_replicate";
   9.132 -val neq_Nil_conv = thm "neq_Nil_conv";
   9.133 -val not_Cons_self = thm "not_Cons_self";
   9.134 -val not_Cons_self2 = thm "not_Cons_self2";
   9.135 -val nth_Cons = thm "nth_Cons";
   9.136 -val nth_Cons' = thm "nth_Cons'";
   9.137 -val nth_Cons_0 = thm "nth_Cons_0";
   9.138 -val nth_Cons_Suc = thm "nth_Cons_Suc";
   9.139 -val nth_append = thm "nth_append";
   9.140 -val nth_drop = thm "nth_drop";
   9.141 -val nth_equalityI = thm "nth_equalityI";
   9.142 -val nth_list_update = thm "nth_list_update";
   9.143 -val nth_list_update_eq = thm "nth_list_update_eq";
   9.144 -val nth_list_update_neq = thm "nth_list_update_neq";
   9.145 -val nth_map_upt = thm "nth_map_upt";
   9.146 -val nth_mem = thm "nth_mem";
   9.147 -val nth_replicate = thm "nth_replicate";
   9.148 -val nth_take = thm "nth_take";
   9.149 -val nth_take_lemma = thm "nth_take_lemma";
   9.150 -val nth_upt = thm "nth_upt";
   9.151 -val nth_zip = thm "nth_zip";
   9.152 -val replicate_0 = thm "replicate_0";
   9.153 -val replicate_Suc = thm "replicate_Suc";
   9.154 -val replicate_add = thm "replicate_add";
   9.155 -val replicate_app_Cons_same = thm "replicate_app_Cons_same";
   9.156 -val rev_append = thm "rev_append";
   9.157 -val rev_concat = thm "rev_concat";
   9.158 -val rev_drop = thm "rev_drop";
   9.159 -val rev_exhaust = thm "rev_exhaust";
   9.160 -val rev_induct = thm "rev_induct";
   9.161 -val rev_is_Nil_conv = thm "rev_is_Nil_conv";
   9.162 -val rev_is_rev_conv = thm "rev_is_rev_conv";
   9.163 -val rev_map = thm "rev_map";
   9.164 -val rev_replicate = thm "rev_replicate";
   9.165 -val rev_rev_ident = thm "rev_rev_ident";
   9.166 -val rev_take = thm "rev_take";
   9.167 -val same_append_eq = thm "same_append_eq";
   9.168 -val self_append_conv = thm "self_append_conv";
   9.169 -val self_append_conv2 = thm "self_append_conv2";
   9.170 -val set_append = thm "set_append";
   9.171 -val set_concat = thm "set_concat";
   9.172 -val set_conv_nth = thm "set_conv_nth";
   9.173 -val set_empty = thm "set_empty";
   9.174 -val set_filter = thm "set_filter";
   9.175 -val set_map = thm "set_map";
   9.176 -val mem_ii = thm "mem_iff";
   9.177 -val set_remdups = thm "set_remdups";
   9.178 -val set_replicate = thm "set_replicate";
   9.179 -val set_replicate_conv_if = thm "set_replicate_conv_if";
   9.180 -val set_rev = thm "set_rev";
   9.181 -val set_subset_Cons = thm "set_subset_Cons";
   9.182 -val set_take_whileD = thm "set_take_whileD";
   9.183 -val set_update_subsetI = thm "set_update_subsetI";
   9.184 -val set_update_subset_insert = thm "set_update_subset_insert";
   9.185 -val set_upt = thm "set_upt";
   9.186 -val set_zip = thm "set_zip";
   9.187 -val start_le_sum = thm "start_le_sum";
   9.188 -val sublist_Cons = thm "sublist_Cons";
   9.189 -val sublist_append = thm "sublist_append";
   9.190 -val sublist_def = thm "sublist_def";
   9.191 -val sublist_empty = thm "sublist_empty";
   9.192 -val sublist_nil = thm "sublist_nil";
   9.193 -val sublist_shift_lemma = thm "sublist_shift_lemma";
   9.194 -val sublist_singleton = thm "sublist_singleton";
   9.195 -val sublist_upt_eq_take = thm "sublist_upt_eq_take";
   9.196 -val sum_eq_0_conv = thm "sum_eq_0_conv";
   9.197 -val takeWhile_append1 = thm "takeWhile_append1";
   9.198 -val takeWhile_append2 = thm "takeWhile_append2";
   9.199 -val takeWhile_dropWhile_id = thm "takeWhile_dropWhile_id";
   9.200 -val takeWhile_tail = thm "takeWhile_tail";
   9.201 -val take_0 = thm "take_0";
   9.202 -val take_Cons = thm "take_Cons";
   9.203 -val take_Cons' = thm "take_Cons'";
   9.204 -val take_Nil = thm "take_Nil";
   9.205 -val take_Suc_Cons = thm "take_Suc_Cons";
   9.206 -val take_all = thm "take_all";
   9.207 -val take_append = thm "take_append";
   9.208 -val take_drop = thm "take_drop";
   9.209 -val take_equalityI = thm "take_equalityI";
   9.210 -val take_map = thm "take_map"; 
   9.211 -val take_take = thm "take_take";
   9.212 -val take_upt = thm "take_upt";
   9.213 -val tl_append = thm "tl_append";
   9.214 -val tl_append2 = thm "tl_append2";
   9.215 -val tl_replicate = thm "tl_replicate";
   9.216 -val update_zip = thm "update_zip";
   9.217 -val upt_0 = thm "upt_0";
   9.218 -val upt_Suc = thm "upt_Suc";
   9.219 -val upt_Suc_append = thm "upt_Suc_append";
   9.220 -val upt_add_eq_append = thm "upt_add_eq_append";
   9.221 -val upt_conv_Cons = thm "upt_conv_Cons";
   9.222 -val upt_conv_Nil = thm "upt_conv_Nil";
   9.223 -val upt_rec = thm "upt_rec";
   9.224 -val wf_lex = thm "wf_lex";
   9.225 -val wf_lenlex = thm "wf_lenlex";
   9.226 -val wf_lexn = thm "wf_lexn";
   9.227 -val zip_Cons_Cons = thm "zip_Cons_Cons";
   9.228 -val zip_Nil = thm "zip_Nil";
   9.229 -val zip_append = thm "zip_append";
   9.230 -val zip_append1 = thm "zip_append1";
   9.231 -val zip_append2 = thm "zip_append2";
   9.232 -val zip_replicate = thm "zip_replicate";
   9.233 -val zip_rev = thm "zip_rev";
   9.234 -val zip_update = thm "zip_update";
    10.1 --- a/src/HOL/Nat.ML	Tue Dec 05 22:14:53 2006 +0100
    10.2 +++ b/src/HOL/Nat.ML	Wed Dec 06 01:12:36 2006 +0100
    10.3 @@ -17,17 +17,6 @@
    10.4    val simps = thms "nat.simps";
    10.5  end;
    10.6  
    10.7 -val [nat_rec_0, nat_rec_Suc] = thms "nat.recs";
    10.8 -bind_thm ("nat_rec_0", nat_rec_0);
    10.9 -bind_thm ("nat_rec_Suc", nat_rec_Suc);
   10.10 -
   10.11 -val [nat_case_0, nat_case_Suc] = thms "nat.cases";
   10.12 -bind_thm ("nat_case_0", nat_case_0);
   10.13 -bind_thm ("nat_case_Suc", nat_case_Suc);
   10.14 -
   10.15 -val leD = thm "leD";  (*Now defined in Orderings.thy*)
   10.16 -val leI = thm "leI";
   10.17 -
   10.18  val Least_Suc = thm "Least_Suc";
   10.19  val Least_Suc2 = thm "Least_Suc2";
   10.20  val One_nat_def = thm "One_nat_def";
    11.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 05 22:14:53 2006 +0100
    11.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Dec 06 01:12:36 2006 +0100
    11.3 @@ -16,6 +16,10 @@
    11.4  structure NominalAtoms : NOMINAL_ATOMS =
    11.5  struct
    11.6  
    11.7 +val Finites_emptyI = thm "Finites.emptyI";
    11.8 +val Collect_const = thm "Collect_const";
    11.9 +
   11.10 +
   11.11  (* data kind 'HOL/nominal' *)
   11.12  
   11.13  structure NominalArgs =
   11.14 @@ -477,7 +481,7 @@
   11.15                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
   11.16                  else
   11.17                    let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
   11.18 -                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI];
   11.19 +                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites_emptyI];
   11.20                    in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
   11.21          in
   11.22           AxClass.prove_arity (qu_name,[],[qu_class]) proof thy'
   11.23 @@ -614,7 +618,7 @@
   11.24  	     let
   11.25  	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
   11.26  	       val supp_def = thm "Nominal.supp_def";
   11.27 -               val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
   11.28 +               val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites_emptyI,defn];
   11.29                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
   11.30               in 
   11.31  	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    12.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Dec 05 22:14:53 2006 +0100
    12.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Dec 06 01:12:36 2006 +0100
    12.3 @@ -18,6 +18,18 @@
    12.4  structure NominalPackage : NOMINAL_PACKAGE =
    12.5  struct
    12.6  
    12.7 +val Finites_emptyI = thm "Finites.emptyI";
    12.8 +val finite_Diff = thm "finite_Diff";
    12.9 +val finite_Un = thm "finite_Un";
   12.10 +val Un_iff = thm "Un_iff";
   12.11 +val In0_eq = thm "In0_eq";
   12.12 +val In1_eq = thm "In1_eq";
   12.13 +val In0_not_In1 = thm "In0_not_In1";
   12.14 +val In1_not_In0 = thm "In1_not_In0";
   12.15 +val Un_assoc = thm "Un_assoc";
   12.16 +val Collect_disj_eq = thm "Collect_disj_eq";
   12.17 +val empty_def = thm "empty_def";
   12.18 +
   12.19  open DatatypeAux;
   12.20  open NominalAtoms;
   12.21  
   12.22 @@ -1004,7 +1016,7 @@
   12.23              (fn _ =>
   12.24                simp_tac (HOL_basic_ss addsimps (supp_def ::
   12.25                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
   12.26 -                 symmetric empty_def :: Finites.emptyI :: simp_thms @
   12.27 +                 symmetric empty_def :: Finites_emptyI :: simp_thms @
   12.28                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
   12.29          in
   12.30            (supp_thm,
    13.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Tue Dec 05 22:14:53 2006 +0100
    13.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Dec 06 01:12:36 2006 +0100
    13.3 @@ -48,6 +48,9 @@
    13.4  structure NominalPermeq : NOMINAL_PERMEQ =
    13.5  struct
    13.6  
    13.7 +val Finites_emptyI = thm "Finites.emptyI";
    13.8 +val finite_Un = thm "finite_Un";
    13.9 +
   13.10  (* pulls out dynamically a thm via the proof state *)
   13.11  fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
   13.12  fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) (Name name);
   13.13 @@ -278,7 +281,7 @@
   13.14                Logic.strip_assums_concl (hd (prems_of supports_rule'));
   13.15              val supports_rule'' = Drule.cterm_instantiate
   13.16                [(cert (head_of S), cert s')] supports_rule'
   13.17 -            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites.emptyI]
   13.18 +            val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites_emptyI]
   13.19            in
   13.20              (tactical ("guessing of the right supports-set",
   13.21                        EVERY [compose_tac (false, supports_rule'', 2) i,
   13.22 @@ -316,7 +319,7 @@
   13.23              val supports_fresh_rule'' = Drule.cterm_instantiate
   13.24                [(cert (head_of S), cert s')] supports_fresh_rule'
   13.25  	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
   13.26 -            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI]
   13.27 +            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites_emptyI]
   13.28              (* FIXME sometimes these rewrite rules are already in the ss, *)
   13.29              (* which produces a warning                                   *)
   13.30            in
    14.1 --- a/src/HOL/Orderings.ML	Tue Dec 05 22:14:53 2006 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,17 +0,0 @@
    14.4 -(* legacy ML bindings *)
    14.5 -
    14.6 -val order_less_irrefl = thm "order_less_irrefl";
    14.7 -val linorder_not_less = thm "linorder_not_less";
    14.8 -val linorder_not_le = thm "linorder_not_le";
    14.9 -val linorder_neq_iff = thm "linorder_neq_iff";
   14.10 -val linorder_neqE = thm "linorder_neqE";
   14.11 -val order_refl = thm "order_refl";
   14.12 -val order_trans = thm "order_trans";
   14.13 -val order_antisym = thm "order_antisym";
   14.14 -val mono_def = thm "mono_def";
   14.15 -val monoI = thm "monoI";
   14.16 -val monoD = thm "monoD";
   14.17 -val max_less_iff_conj = thm "max_less_iff_conj";
   14.18 -val min_less_iff_conj = thm "min_less_iff_conj";
   14.19 -val split_min = thm "split_min";
   14.20 -val split_max = thm "split_max";
    15.1 --- a/src/HOL/Relation.ML	Tue Dec 05 22:14:53 2006 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,100 +0,0 @@
    15.4 -
    15.5 -(* legacy ML bindings *)
    15.6 -
    15.7 -val DomainE = thm "DomainE";
    15.8 -val DomainI = thm "DomainI";
    15.9 -val Domain_Collect_split = thm "Domain_Collect_split";
   15.10 -val Domain_Diff_subset = thm "Domain_Diff_subset";
   15.11 -val Domain_Id = thm "Domain_Id";
   15.12 -val Domain_Int_subset = thm "Domain_Int_subset";
   15.13 -val Domain_Un_eq = thm "Domain_Un_eq";
   15.14 -val Domain_Union = thm "Domain_Union";
   15.15 -val Domain_def = thm "Domain_def";
   15.16 -val Domain_diag = thm "Domain_diag";
   15.17 -val Domain_empty = thm "Domain_empty";
   15.18 -val Domain_iff = thm "Domain_iff";
   15.19 -val Domain_insert = thm "Domain_insert";
   15.20 -val Domain_mono = thm "Domain_mono";
   15.21 -val Field_def = thm "Field_def";
   15.22 -val IdE = thm "IdE";
   15.23 -val IdI = thm "IdI";
   15.24 -val Id_O_R = thm "Id_O_R";
   15.25 -val Id_def = thm "Id_def";
   15.26 -val ImageE = thm "ImageE";
   15.27 -val ImageI = thm "ImageI";
   15.28 -val Image_Collect_split = thm "Image_Collect_split";
   15.29 -val Image_INT_subset = thm "Image_INT_subset";
   15.30 -val Image_Id = thm "Image_Id";
   15.31 -val Image_Int_subset = thm "Image_Int_subset";
   15.32 -val Image_UN = thm "Image_UN";
   15.33 -val Image_Un = thm "Image_Un";
   15.34 -val Image_def = thm "Image_def";
   15.35 -val Image_diag = thm "Image_diag";
   15.36 -val Image_empty = thm "Image_empty";
   15.37 -val Image_eq_UN = thm "Image_eq_UN";
   15.38 -val Image_iff = thm "Image_iff";
   15.39 -val Image_mono = thm "Image_mono";
   15.40 -val Image_singleton = thm "Image_singleton";
   15.41 -val Image_singleton_iff = thm "Image_singleton_iff";
   15.42 -val Image_subset = thm "Image_subset";
   15.43 -val Image_subset_eq = thm "Image_subset_eq";
   15.44 -val O_assoc = thm "O_assoc";
   15.45 -val R_O_Id = thm "R_O_Id";
   15.46 -val RangeE = thm "RangeE";
   15.47 -val RangeI = thm "RangeI";
   15.48 -val Range_Collect_split = thm "Range_Collect_split";
   15.49 -val Range_Diff_subset = thm "Range_Diff_subset";
   15.50 -val Range_Id = thm "Range_Id";
   15.51 -val Range_Int_subset = thm "Range_Int_subset";
   15.52 -val Range_Un_eq = thm "Range_Un_eq";
   15.53 -val Range_Union = thm "Range_Union";
   15.54 -val Range_def = thm "Range_def";
   15.55 -val Range_diag = thm "Range_diag";
   15.56 -val Range_empty = thm "Range_empty";
   15.57 -val Range_iff = thm "Range_iff";
   15.58 -val Range_insert = thm "Range_insert";
   15.59 -val antisymD = thm "antisymD";
   15.60 -val antisymI = thm "antisymI";
   15.61 -val antisym_Id = thm "antisym_Id";
   15.62 -val antisym_converse = thm "antisym_converse";
   15.63 -val antisym_def = thm "antisym_def";
   15.64 -val converseD = thm "converseD";
   15.65 -val converseE = thm "converseE";
   15.66 -val converseI = thm "converseI";
   15.67 -val converse_Id = thm "converse_Id";
   15.68 -val converse_converse = thm "converse_converse";
   15.69 -val converse_def = thm "converse_def";
   15.70 -val converse_diag = thm "converse_diag";
   15.71 -val converse_iff = thm "converse_iff";
   15.72 -val converse_rel_comp = thm "converse_rel_comp";
   15.73 -val diagE = thm "diagE";
   15.74 -val diagI = thm "diagI";
   15.75 -val diag_def = thm "diag_def";
   15.76 -val diag_eqI = thm "diag_eqI";
   15.77 -val diag_iff = thm "diag_iff";
   15.78 -val diag_subset_Times = thm "diag_subset_Times";
   15.79 -val inv_image_def = thm "inv_image_def";
   15.80 -val pair_in_Id_conv = thm "pair_in_Id_conv";
   15.81 -val reflD = thm "reflD";
   15.82 -val reflI = thm "reflI";
   15.83 -val refl_converse = thm "refl_converse";
   15.84 -val refl_def = thm "refl_def";
   15.85 -val reflexive_Id = thm "reflexive_Id";
   15.86 -val rel_compE = thm "rel_compE";
   15.87 -val rel_compEpair = thm "rel_compEpair";
   15.88 -val rel_compI = thm "rel_compI";
   15.89 -val rel_comp_def = thm "rel_comp_def";
   15.90 -val rel_comp_mono = thm "rel_comp_mono";
   15.91 -val rel_comp_subset_Sigma = thm "rel_comp_subset_Sigma";
   15.92 -val rev_ImageI = thm "rev_ImageI";
   15.93 -val single_valuedD = thm "single_valuedD";
   15.94 -val single_valuedI = thm "single_valuedI";
   15.95 -val single_valued_def = thm "single_valued_def";
   15.96 -val sym_def = thm "sym_def";
   15.97 -val transD = thm "transD";
   15.98 -val transI = thm "transI";
   15.99 -val trans_Id = thm "trans_Id";
  15.100 -val trans_O_subset = thm "trans_O_subset";
  15.101 -val trans_converse = thm "trans_converse";
  15.102 -val trans_def = thm "trans_def";
  15.103 -val trans_inv_image = thm "trans_inv_image";
    16.1 --- a/src/HOL/Set.ML	Tue Dec 05 22:14:53 2006 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,433 +0,0 @@
    16.4 -
    16.5 -(* legacy ML bindings *)
    16.6 -
    16.7 -val Ball_def = thm "Ball_def";
    16.8 -val Bex_def = thm "Bex_def";
    16.9 -val CollectD = thm "CollectD";
   16.10 -val CollectE = thm "CollectE";
   16.11 -val CollectI = thm "CollectI";
   16.12 -val Collect_all_eq = thm "Collect_all_eq";
   16.13 -val Collect_ball_eq = thm "Collect_ball_eq";
   16.14 -val Collect_bex_eq = thm "Collect_bex_eq";
   16.15 -val Collect_cong = thm "Collect_cong";
   16.16 -val Collect_conj_eq = thm "Collect_conj_eq";
   16.17 -val Collect_const = thm "Collect_const";
   16.18 -val Collect_disj_eq = thm "Collect_disj_eq";
   16.19 -val Collect_empty_eq = thm "Collect_empty_eq";
   16.20 -val Collect_ex_eq = thm "Collect_ex_eq";
   16.21 -val Collect_mem_eq = thm "Collect_mem_eq";
   16.22 -val Collect_mono = thm "Collect_mono";
   16.23 -val Collect_neg_eq = thm "Collect_neg_eq";
   16.24 -val ComplD = thm "ComplD";
   16.25 -val ComplE = thm "ComplE";
   16.26 -val ComplI = thm "ComplI";
   16.27 -val Compl_Diff_eq = thm "Compl_Diff_eq";
   16.28 -val Compl_INT = thm "Compl_INT";
   16.29 -val Compl_Int = thm "Compl_Int";
   16.30 -val Compl_UN = thm "Compl_UN";
   16.31 -val Compl_UNIV_eq = thm "Compl_UNIV_eq";
   16.32 -val Compl_Un = thm "Compl_Un";
   16.33 -val Compl_anti_mono = thm "Compl_anti_mono";
   16.34 -val Compl_def = thm "Compl_def";
   16.35 -val Compl_disjoint = thm "Compl_disjoint";
   16.36 -val Compl_disjoint2 = thm "Compl_disjoint2";
   16.37 -val Compl_empty_eq = thm "Compl_empty_eq";
   16.38 -val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff";
   16.39 -val Compl_iff = thm "Compl_iff";
   16.40 -val Compl_partition = thm "Compl_partition";
   16.41 -val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff";
   16.42 -val DiffD1 = thm "DiffD1";
   16.43 -val DiffD2 = thm "DiffD2";
   16.44 -val DiffE = thm "DiffE";
   16.45 -val DiffI = thm "DiffI";
   16.46 -val Diff_Compl = thm "Diff_Compl";
   16.47 -val Diff_Int = thm "Diff_Int";
   16.48 -val Diff_Int_distrib = thm "Diff_Int_distrib";
   16.49 -val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
   16.50 -val Diff_UNIV = thm "Diff_UNIV";
   16.51 -val Diff_Un = thm "Diff_Un";
   16.52 -val Diff_cancel = thm "Diff_cancel";
   16.53 -val Diff_disjoint = thm "Diff_disjoint";
   16.54 -val Diff_empty = thm "Diff_empty";
   16.55 -val Diff_eq = thm "Diff_eq";
   16.56 -val Diff_eq_empty_iff = thm "Diff_eq_empty_iff";
   16.57 -val Diff_iff = thm "Diff_iff";
   16.58 -val Diff_insert = thm "Diff_insert";
   16.59 -val Diff_insert0 = thm "Diff_insert0";
   16.60 -val Diff_insert2 = thm "Diff_insert2";
   16.61 -val Diff_insert_absorb = thm "Diff_insert_absorb";
   16.62 -val Diff_mono = thm "Diff_mono";
   16.63 -val Diff_partition = thm "Diff_partition";
   16.64 -val Diff_subset = thm "Diff_subset";
   16.65 -val Diff_triv = thm "Diff_triv";
   16.66 -val INTER_def = thm "INTER_def";
   16.67 -val INT_D = thm "INT_D";
   16.68 -val INT_E = thm "INT_E";
   16.69 -val INT_I = thm "INT_I";
   16.70 -val INT_Int_distrib = thm "INT_Int_distrib";
   16.71 -val INT_Un = thm "INT_Un";
   16.72 -val INT_absorb = thm "INT_absorb";
   16.73 -val INT_anti_mono = thm "INT_anti_mono";
   16.74 -val INT_bool_eq = thm "INT_bool_eq";
   16.75 -val INT_cong = thm "INT_cong";
   16.76 -val INT_constant = thm "INT_constant";
   16.77 -val INT_empty = thm "INT_empty";
   16.78 -val INT_eq = thm "INT_eq";
   16.79 -val INT_greatest = thm "INT_greatest";
   16.80 -val INT_iff = thm "INT_iff";
   16.81 -val INT_insert = thm "INT_insert";
   16.82 -val INT_insert_distrib = thm "INT_insert_distrib";
   16.83 -val INT_lower = thm "INT_lower";
   16.84 -val INT_simps = thms "INT_simps";
   16.85 -val INT_subset_iff = thm "INT_subset_iff";
   16.86 -val IntD1 = thm "IntD1";
   16.87 -val IntD2 = thm "IntD2";
   16.88 -val IntE = thm "IntE";
   16.89 -val IntI = thm "IntI";
   16.90 -val Int_Collect = thm "Int_Collect";
   16.91 -val Int_Collect_mono = thm "Int_Collect_mono";
   16.92 -val Int_Diff = thm "Int_Diff";
   16.93 -val Int_Inter_image = thm "Int_Inter_image";
   16.94 -val Int_UNIV = thm "Int_UNIV";
   16.95 -val Int_UNIV_left = thm "Int_UNIV_left";
   16.96 -val Int_UNIV_right = thm "Int_UNIV_right";
   16.97 -val Int_UN_distrib = thm "Int_UN_distrib";
   16.98 -val Int_UN_distrib2 = thm "Int_UN_distrib2";
   16.99 -val Int_Un_distrib = thm "Int_Un_distrib";
  16.100 -val Int_Un_distrib2 = thm "Int_Un_distrib2";
  16.101 -val Int_Union = thm "Int_Union";
  16.102 -val Int_Union2 = thm "Int_Union2";
  16.103 -val Int_absorb = thm "Int_absorb";
  16.104 -val Int_absorb1 = thm "Int_absorb1";
  16.105 -val Int_absorb2 = thm "Int_absorb2";
  16.106 -val Int_ac = thms "Int_ac";
  16.107 -val Int_assoc = thm "Int_assoc";
  16.108 -val Int_commute = thm "Int_commute";
  16.109 -val Int_def = thm "Int_def";
  16.110 -val Int_empty_left = thm "Int_empty_left";
  16.111 -val Int_empty_right = thm "Int_empty_right";
  16.112 -val Int_eq_Inter = thm "Int_eq_Inter";
  16.113 -val Int_greatest = thm "Int_greatest";
  16.114 -val Int_iff = thm "Int_iff";
  16.115 -val Int_insert_left = thm "Int_insert_left";
  16.116 -val Int_insert_right = thm "Int_insert_right";
  16.117 -val Int_left_absorb = thm "Int_left_absorb";
  16.118 -val Int_left_commute = thm "Int_left_commute";
  16.119 -val Int_lower1 = thm "Int_lower1";
  16.120 -val Int_lower2 = thm "Int_lower2";
  16.121 -val Int_mono = thm "Int_mono";
  16.122 -val Int_subset_iff = thm "Int_subset_iff";
  16.123 -val InterD = thm "InterD";
  16.124 -val InterE = thm "InterE";
  16.125 -val InterI = thm "InterI";
  16.126 -val Inter_UNIV = thm "Inter_UNIV";
  16.127 -val Inter_Un_distrib = thm "Inter_Un_distrib";
  16.128 -val Inter_Un_subset = thm "Inter_Un_subset";
  16.129 -val Inter_anti_mono = thm "Inter_anti_mono";
  16.130 -val Inter_def = thm "Inter_def";
  16.131 -val Inter_empty = thm "Inter_empty";
  16.132 -val Inter_greatest = thm "Inter_greatest";
  16.133 -val Inter_iff = thm "Inter_iff";
  16.134 -val Inter_image_eq = thm "Inter_image_eq";
  16.135 -val Inter_insert = thm "Inter_insert";
  16.136 -val Inter_lower = thm "Inter_lower";
  16.137 -val PowD = thm "PowD";
  16.138 -val PowI = thm "PowI";
  16.139 -val Pow_Compl = thm "Pow_Compl";
  16.140 -val Pow_INT_eq = thm "Pow_INT_eq";
  16.141 -val Pow_Int_eq = thm "Pow_Int_eq";
  16.142 -val Pow_UNIV = thm "Pow_UNIV";
  16.143 -val Pow_bottom = thm "Pow_bottom";
  16.144 -val Pow_def = thm "Pow_def";
  16.145 -val Pow_empty = thm "Pow_empty";
  16.146 -val Pow_iff = thm "Pow_iff";
  16.147 -val Pow_insert = thm "Pow_insert";
  16.148 -val Pow_mono = thm "Pow_mono";
  16.149 -val Pow_top = thm "Pow_top";
  16.150 -val UNION_def = thm "UNION_def";
  16.151 -val UNIV_I = thm "UNIV_I";
  16.152 -val UNIV_def = thm "UNIV_def";
  16.153 -val UNIV_not_empty = thm "UNIV_not_empty";
  16.154 -val UNIV_witness = thm "UNIV_witness";
  16.155 -val UN_E = thm "UN_E";
  16.156 -val UN_I = thm "UN_I";
  16.157 -val UN_Pow_subset = thm "UN_Pow_subset";
  16.158 -val UN_UN_flatten = thm "UN_UN_flatten";
  16.159 -val UN_Un = thm "UN_Un";
  16.160 -val UN_Un_distrib = thm "UN_Un_distrib";
  16.161 -val UN_absorb = thm "UN_absorb";
  16.162 -val UN_bool_eq = thm "UN_bool_eq";
  16.163 -val UN_cong = thm "UN_cong";
  16.164 -val UN_constant = thm "UN_constant";
  16.165 -val UN_empty = thm "UN_empty";
  16.166 -val UN_empty2 = thm "UN_empty2";
  16.167 -val UN_eq = thm "UN_eq";
  16.168 -val UN_iff = thm "UN_iff";
  16.169 -val UN_insert = thm "UN_insert";
  16.170 -val UN_insert_distrib = thm "UN_insert_distrib";
  16.171 -val UN_least = thm "UN_least";
  16.172 -val UN_mono = thm "UN_mono";
  16.173 -val UN_simps = thms "UN_simps";
  16.174 -val UN_singleton = thm "UN_singleton";
  16.175 -val UN_subset_iff = thm "UN_subset_iff";
  16.176 -val UN_upper = thm "UN_upper";
  16.177 -val UnCI = thm "UnCI";
  16.178 -val UnE = thm "UnE";
  16.179 -val UnI1 = thm "UnI1";
  16.180 -val UnI2 = thm "UnI2";
  16.181 -val Un_Diff = thm "Un_Diff";
  16.182 -val Un_Diff_Int = thm "Un_Diff_Int";
  16.183 -val Un_Diff_cancel = thm "Un_Diff_cancel";
  16.184 -val Un_Diff_cancel2 = thm "Un_Diff_cancel2";
  16.185 -val Un_INT_distrib = thm "Un_INT_distrib";
  16.186 -val Un_INT_distrib2 = thm "Un_INT_distrib2";
  16.187 -val Un_Int_assoc_eq = thm "Un_Int_assoc_eq";
  16.188 -val Un_Int_crazy = thm "Un_Int_crazy";
  16.189 -val Un_Int_distrib = thm "Un_Int_distrib";
  16.190 -val Un_Int_distrib2 = thm "Un_Int_distrib2";
  16.191 -val Un_Inter = thm "Un_Inter";
  16.192 -val Un_Pow_subset = thm "Un_Pow_subset";
  16.193 -val Un_UNIV_left = thm "Un_UNIV_left";
  16.194 -val Un_UNIV_right = thm "Un_UNIV_right";
  16.195 -val Un_Union_image = thm "Un_Union_image";
  16.196 -val Un_absorb = thm "Un_absorb";
  16.197 -val Un_absorb1 = thm "Un_absorb1";
  16.198 -val Un_absorb2 = thm "Un_absorb2";
  16.199 -val Un_ac = thms "Un_ac";
  16.200 -val Un_assoc = thm "Un_assoc";
  16.201 -val Un_commute = thm "Un_commute";
  16.202 -val Un_def = thm "Un_def";
  16.203 -val Un_empty = thm "Un_empty";
  16.204 -val Un_empty_left = thm "Un_empty_left";
  16.205 -val Un_empty_right = thm "Un_empty_right";
  16.206 -val Un_eq_UN = thm "Un_eq_UN";
  16.207 -val Un_eq_Union = thm "Un_eq_Union";
  16.208 -val Un_iff = thm "Un_iff";
  16.209 -val Un_insert_left = thm "Un_insert_left";
  16.210 -val Un_insert_right = thm "Un_insert_right";
  16.211 -val Un_least = thm "Un_least";
  16.212 -val Un_left_absorb = thm "Un_left_absorb";
  16.213 -val Un_left_commute = thm "Un_left_commute";
  16.214 -val Un_mono = thm "Un_mono";
  16.215 -val Un_subset_iff = thm "Un_subset_iff";
  16.216 -val Un_upper1 = thm "Un_upper1";
  16.217 -val Un_upper2 = thm "Un_upper2";
  16.218 -val UnionE = thm "UnionE";
  16.219 -val UnionI = thm "UnionI";
  16.220 -val Union_Int_subset = thm "Union_Int_subset";
  16.221 -val Union_Pow_eq = thm "Union_Pow_eq";
  16.222 -val Union_UNIV = thm "Union_UNIV";
  16.223 -val Union_Un_distrib = thm "Union_Un_distrib";
  16.224 -val Union_def = thm "Union_def";
  16.225 -val Union_disjoint = thm "Union_disjoint";
  16.226 -val Union_empty = thm "Union_empty";
  16.227 -val Union_empty_conv = thm "Union_empty_conv";
  16.228 -val Union_iff = thm "Union_iff";
  16.229 -val Union_image_eq = thm "Union_image_eq";
  16.230 -val Union_insert = thm "Union_insert";
  16.231 -val Union_least = thm "Union_least";
  16.232 -val Union_mono = thm "Union_mono";
  16.233 -val Union_upper = thm "Union_upper";
  16.234 -val all_bool_eq = thm "all_bool_eq";
  16.235 -val all_mono = thm "all_mono";
  16.236 -val all_not_in_conv = thm "all_not_in_conv";
  16.237 -val atomize_ball = thm "atomize_ball";
  16.238 -val ballE = thm "ballE";
  16.239 -val ballI = thm "ballI";
  16.240 -val ball_UN = thm "ball_UN";
  16.241 -val ball_UNIV = thm "ball_UNIV";
  16.242 -val ball_Un = thm "ball_Un";
  16.243 -val ball_cong = thm "ball_cong";
  16.244 -val ball_conj_distrib = thm "ball_conj_distrib";
  16.245 -val ball_empty = thm "ball_empty";
  16.246 -val ball_one_point1 = thm "ball_one_point1";
  16.247 -val ball_one_point2 = thm "ball_one_point2";
  16.248 -val ball_simps = thms "ball_simps";
  16.249 -val ball_triv = thm "ball_triv";
  16.250 -val basic_monos = thms "basic_monos";
  16.251 -val bexCI = thm "bexCI";
  16.252 -val bexE = thm "bexE";
  16.253 -val bexI = thm "bexI";
  16.254 -val bex_UN = thm "bex_UN";
  16.255 -val bex_UNIV = thm "bex_UNIV";
  16.256 -val bex_Un = thm "bex_Un";
  16.257 -val bex_cong = thm "bex_cong";
  16.258 -val bex_disj_distrib = thm "bex_disj_distrib";
  16.259 -val bex_empty = thm "bex_empty";
  16.260 -val bex_one_point1 = thm "bex_one_point1";
  16.261 -val bex_one_point2 = thm "bex_one_point2";
  16.262 -val bex_simps = thms "bex_simps";
  16.263 -val bex_triv = thm "bex_triv";
  16.264 -val bex_triv_one_point1 = thm "bex_triv_one_point1";
  16.265 -val bex_triv_one_point2 = thm "bex_triv_one_point2";
  16.266 -val bool_induct = thm "bool_induct";
  16.267 -val bspec = thm "bspec";
  16.268 -val conj_mono = thm "conj_mono";
  16.269 -val contra_subsetD = thm "contra_subsetD";
  16.270 -val diff_single_insert = thm "diff_single_insert";
  16.271 -val disj_mono = thm "disj_mono";
  16.272 -val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl";
  16.273 -val disjoint_iff_not_equal = thm "disjoint_iff_not_equal";
  16.274 -val distinct_lemma = thm "distinct_lemma";
  16.275 -val double_complement = thm "double_complement";
  16.276 -val double_diff = thm "double_diff";
  16.277 -val emptyE = thm "emptyE";
  16.278 -val empty_Diff = thm "empty_Diff";
  16.279 -val empty_def = thm "empty_def";
  16.280 -val empty_iff = thm "empty_iff";
  16.281 -val empty_subsetI = thm "empty_subsetI";
  16.282 -val eq_to_mono = thm "eq_to_mono";
  16.283 -val eq_to_mono2 = thm "eq_to_mono2";
  16.284 -val eqset_imp_iff = thm "eqset_imp_iff";
  16.285 -val equalityCE = thm "equalityCE";
  16.286 -val equalityD1 = thm "equalityD1";
  16.287 -val equalityD2 = thm "equalityD2";
  16.288 -val equalityE = thm "equalityE";
  16.289 -val equalityI = thm "equalityI";
  16.290 -val equals0D = thm "equals0D";
  16.291 -val equals0I = thm "equals0I";
  16.292 -val ex_bool_eq = thm "ex_bool_eq";
  16.293 -val ex_mono = thm "ex_mono";
  16.294 -val full_SetCompr_eq = thm "full_SetCompr_eq";
  16.295 -val if_image_distrib = thm "if_image_distrib";
  16.296 -val imageE = thm "imageE";
  16.297 -val imageI = thm "imageI";
  16.298 -val image_Collect = thm "image_Collect";
  16.299 -val image_Un = thm "image_Un";
  16.300 -val image_Union = thm "image_Union";
  16.301 -val image_cong = thm "image_cong";
  16.302 -val image_constant = thm "image_constant";
  16.303 -val image_def = thm "image_def";
  16.304 -val image_empty = thm "image_empty";
  16.305 -val image_eqI = thm "image_eqI";
  16.306 -val image_iff = thm "image_iff";
  16.307 -val image_image = thm "image_image";
  16.308 -val image_insert = thm "image_insert";
  16.309 -val image_is_empty = thm "image_is_empty";
  16.310 -val image_mono = thm "image_mono";
  16.311 -val image_subsetI = thm "image_subsetI";
  16.312 -val image_subset_iff = thm "image_subset_iff";
  16.313 -val imp_mono = thm "imp_mono";
  16.314 -val imp_refl = thm "imp_refl";
  16.315 -val in_mono = thm "in_mono";
  16.316 -val insertCI = thm "insertCI";
  16.317 -val insertE = thm "insertE";
  16.318 -val insertI1 = thm "insertI1";
  16.319 -val insertI2 = thm "insertI2";
  16.320 -val insert_Collect = thm "insert_Collect";
  16.321 -val insert_Diff = thm "insert_Diff";
  16.322 -val insert_Diff1 = thm "insert_Diff1";
  16.323 -val insert_Diff_if = thm "insert_Diff_if";
  16.324 -val insert_absorb = thm "insert_absorb";
  16.325 -val insert_absorb2 = thm "insert_absorb2";
  16.326 -val insert_commute = thm "insert_commute";
  16.327 -val insert_def = thm "insert_def";
  16.328 -val insert_iff = thm "insert_iff";
  16.329 -val insert_image = thm "insert_image";
  16.330 -val insert_is_Un = thm "insert_is_Un";
  16.331 -val insert_mono = thm "insert_mono";
  16.332 -val insert_not_empty = thm "insert_not_empty";
  16.333 -val insert_subset = thm "insert_subset";
  16.334 -val mem_Collect_eq = thm "mem_Collect_eq";
  16.335 -val mem_simps = thms "mem_simps";
  16.336 -val mk_disjoint_insert = thm "mk_disjoint_insert";
  16.337 -val mono_Int = thm "mono_Int";
  16.338 -val mono_Un = thm "mono_Un";
  16.339 -val not_psubset_empty = thm "not_psubset_empty";
  16.340 -val psubsetI = thm "psubsetI";
  16.341 -val psubset_def = thm "psubset_def";
  16.342 -val psubset_eq = thm "psubset_eq";
  16.343 -val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
  16.344 -val psubset_imp_subset = thm "psubset_imp_subset";
  16.345 -val psubset_insert_iff = thm "psubset_insert_iff";
  16.346 -val psubset_subset_trans = thm "psubset_subset_trans";
  16.347 -val rangeE = thm "rangeE";
  16.348 -val rangeI = thm "rangeI";
  16.349 -val range_composition = thm "range_composition";
  16.350 -val range_eqI = thm "range_eqI";
  16.351 -val rev_bexI = thm "rev_bexI";
  16.352 -val rev_image_eqI = thm "rev_image_eqI";
  16.353 -val rev_subsetD = thm "rev_subsetD";
  16.354 -val set_diff_def = thm "set_diff_def";
  16.355 -val set_eq_subset = thm "set_eq_subset";
  16.356 -val set_ext = thm "set_ext";
  16.357 -val singletonD = thm "singletonD";
  16.358 -val singletonE = thm "singletonE";
  16.359 -val singletonI = thm "singletonI";
  16.360 -val singleton_conv = thm "singleton_conv";
  16.361 -val singleton_conv2 = thm "singleton_conv2";
  16.362 -val singleton_iff = thm "singleton_iff";
  16.363 -val singleton_inject = thm "singleton_inject";
  16.364 -val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
  16.365 -val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
  16.366 -val split_if_eq1 = thm "split_if_eq1";
  16.367 -val split_if_eq2 = thm "split_if_eq2";
  16.368 -val split_if_mem1 = thm "split_if_mem1";
  16.369 -val split_if_mem2 = thm "split_if_mem2";
  16.370 -val split_ifs = thms "split_ifs";
  16.371 -val strip = thms "strip";
  16.372 -val subsetCE = thm "subsetCE";
  16.373 -val subsetD = thm "subsetD";
  16.374 -val subsetI = thm "subsetI";
  16.375 -val subset_Compl_self_eq = thm "subset_Compl_self_eq";
  16.376 -val subset_Pow_Union = thm "subset_Pow_Union";
  16.377 -val subset_UNIV = thm "subset_UNIV";
  16.378 -val subset_Un_eq = thm "subset_Un_eq";
  16.379 -val subset_antisym = thm "subset_antisym";
  16.380 -val subset_def = thm "subset_def";
  16.381 -val subset_empty = thm "subset_empty";
  16.382 -val subset_iff = thm "subset_iff";
  16.383 -val subset_iff_psubset_eq = thm "subset_iff_psubset_eq";
  16.384 -val subset_image_iff = thm "subset_image_iff";
  16.385 -val subset_insert = thm "subset_insert";
  16.386 -val subset_insertI = thm "subset_insertI";
  16.387 -val subset_insert_iff = thm "subset_insert_iff";
  16.388 -val subset_psubset_trans = thm "subset_psubset_trans";
  16.389 -val subset_refl = thm "subset_refl";
  16.390 -val subset_singletonD = thm "subset_singletonD";
  16.391 -val subset_trans = thm "subset_trans";
  16.392 -val vimageD = thm "vimageD";
  16.393 -val vimageE = thm "vimageE";
  16.394 -val vimageI = thm "vimageI";
  16.395 -val vimageI2 = thm "vimageI2";
  16.396 -val vimage_Collect = thm "vimage_Collect";
  16.397 -val vimage_Collect_eq = thm "vimage_Collect_eq";
  16.398 -val vimage_Compl = thm "vimage_Compl";
  16.399 -val vimage_Diff = thm "vimage_Diff";
  16.400 -val vimage_INT = thm "vimage_INT";
  16.401 -val vimage_Int = thm "vimage_Int";
  16.402 -val vimage_UN = thm "vimage_UN";
  16.403 -val vimage_UNIV = thm "vimage_UNIV";
  16.404 -val vimage_Un = thm "vimage_Un";
  16.405 -val vimage_Union = thm "vimage_Union";
  16.406 -val vimage_def = thm "vimage_def";
  16.407 -val vimage_empty = thm "vimage_empty";
  16.408 -val vimage_eq = thm "vimage_eq";
  16.409 -val vimage_eq_UN = thm "vimage_eq_UN";
  16.410 -val vimage_insert = thm "vimage_insert";
  16.411 -val vimage_mono = thm "vimage_mono";
  16.412 -val vimage_singleton_eq = thm "vimage_singleton_eq";
  16.413 -
  16.414 -structure Set =
  16.415 -struct
  16.416 -  val thy = the_context ();
  16.417 -  val Ball_def = Ball_def;
  16.418 -  val Bex_def = Bex_def;
  16.419 -  val Collect_mem_eq = Collect_mem_eq;
  16.420 -  val Compl_def = Compl_def;
  16.421 -  val INTER_def = INTER_def;
  16.422 -  val Int_def = Int_def;
  16.423 -  val Inter_def = Inter_def;
  16.424 -  val Pow_def = Pow_def;
  16.425 -  val UNION_def = UNION_def;
  16.426 -  val UNIV_def = UNIV_def;
  16.427 -  val Un_def = Un_def;
  16.428 -  val Union_def = Union_def;
  16.429 -  val empty_def = empty_def;
  16.430 -  val image_def = image_def;
  16.431 -  val insert_def = insert_def;
  16.432 -  val mem_Collect_eq = mem_Collect_eq;
  16.433 -  val psubset_def = psubset_def;
  16.434 -  val set_diff_def = set_diff_def;
  16.435 -  val subset_def = subset_def;
  16.436 -end;
    17.1 --- a/src/HOL/Set.thy	Tue Dec 05 22:14:53 2006 +0100
    17.2 +++ b/src/HOL/Set.thy	Wed Dec 06 01:12:36 2006 +0100
    17.3 @@ -2110,4 +2110,65 @@
    17.4  lemmas basic_trans_rules [trans] =
    17.5    order_trans_rules set_rev_mp set_mp
    17.6  
    17.7 +
    17.8 +subsection {* Basic ML bindings *}
    17.9 +
   17.10 +ML {*
   17.11 +val Ball_def = thm "Ball_def";
   17.12 +val Bex_def = thm "Bex_def";
   17.13 +val CollectD = thm "CollectD";
   17.14 +val CollectE = thm "CollectE";
   17.15 +val CollectI = thm "CollectI";
   17.16 +val Collect_conj_eq = thm "Collect_conj_eq";
   17.17 +val Collect_mem_eq = thm "Collect_mem_eq";
   17.18 +val IntD1 = thm "IntD1";
   17.19 +val IntD2 = thm "IntD2";
   17.20 +val IntE = thm "IntE";
   17.21 +val IntI = thm "IntI";
   17.22 +val Int_Collect = thm "Int_Collect";
   17.23 +val UNIV_I = thm "UNIV_I";
   17.24 +val UNIV_witness = thm "UNIV_witness";
   17.25 +val UnE = thm "UnE";
   17.26 +val UnI1 = thm "UnI1";
   17.27 +val UnI2 = thm "UnI2";
   17.28 +val ballE = thm "ballE";
   17.29 +val ballI = thm "ballI";
   17.30 +val bexCI = thm "bexCI";
   17.31 +val bexE = thm "bexE";
   17.32 +val bexI = thm "bexI";
   17.33 +val bex_triv = thm "bex_triv";
   17.34 +val bspec = thm "bspec";
   17.35 +val contra_subsetD = thm "contra_subsetD";
   17.36 +val distinct_lemma = thm "distinct_lemma";
   17.37 +val eq_to_mono = thm "eq_to_mono";
   17.38 +val eq_to_mono2 = thm "eq_to_mono2";
   17.39 +val equalityCE = thm "equalityCE";
   17.40 +val equalityD1 = thm "equalityD1";
   17.41 +val equalityD2 = thm "equalityD2";
   17.42 +val equalityE = thm "equalityE";
   17.43 +val equalityI = thm "equalityI";
   17.44 +val imageE = thm "imageE";
   17.45 +val imageI = thm "imageI";
   17.46 +val image_Un = thm "image_Un";
   17.47 +val image_insert = thm "image_insert";
   17.48 +val insert_commute = thm "insert_commute";
   17.49 +val insert_iff = thm "insert_iff";
   17.50 +val mem_Collect_eq = thm "mem_Collect_eq";
   17.51 +val rangeE = thm "rangeE";
   17.52 +val rangeI = thm "rangeI";
   17.53 +val range_eqI = thm "range_eqI";
   17.54 +val subsetCE = thm "subsetCE";
   17.55 +val subsetD = thm "subsetD";
   17.56 +val subsetI = thm "subsetI";
   17.57 +val subset_refl = thm "subset_refl";
   17.58 +val subset_trans = thm "subset_trans";
   17.59 +val vimageD = thm "vimageD";
   17.60 +val vimageE = thm "vimageE";
   17.61 +val vimageI = thm "vimageI";
   17.62 +val vimageI2 = thm "vimageI2";
   17.63 +val vimage_Collect = thm "vimage_Collect";
   17.64 +val vimage_Int = thm "vimage_Int";
   17.65 +val vimage_Un = thm "vimage_Un";
   17.66 +*}
   17.67 +
   17.68  end
    18.1 --- a/src/HOL/Transitive_Closure.ML	Tue Dec 05 22:14:53 2006 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,50 +0,0 @@
    18.4 -
    18.5 -(* legacy ML bindings *)
    18.6 -
    18.7 -val converse_rtranclE = thm "converse_rtranclE";
    18.8 -val converse_rtranclE2 = thm "converse_rtranclE2";
    18.9 -val converse_rtrancl_induct = thm "converse_rtrancl_induct";
   18.10 -val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2";
   18.11 -val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl";
   18.12 -val converse_trancl_induct = thm "converse_trancl_induct";
   18.13 -val irrefl_tranclI = thm "irrefl_tranclI";
   18.14 -val irrefl_trancl_rD = thm "irrefl_trancl_rD";
   18.15 -val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq";
   18.16 -val r_into_rtrancl = thm "r_into_rtrancl";
   18.17 -val r_into_trancl = thm "r_into_trancl";
   18.18 -val rtranclE = thm "rtranclE";
   18.19 -val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
   18.20 -val rtrancl_converse = thm "rtrancl_converse";
   18.21 -val rtrancl_converseD = thm "rtrancl_converseD";
   18.22 -val rtrancl_converseI = thm "rtrancl_converseI";
   18.23 -val rtrancl_idemp = thm "rtrancl_idemp";
   18.24 -val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp";
   18.25 -val rtrancl_induct = thm "rtrancl_induct";
   18.26 -val rtrancl_induct2 = thm "rtrancl_induct2";
   18.27 -val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
   18.28 -val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
   18.29 -val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
   18.30 -val rtrancl_mono = thm "rtrancl_mono";
   18.31 -val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id";
   18.32 -val rtrancl_refl = thm "rtrancl_refl";
   18.33 -val rtrancl_reflcl = thm "rtrancl_reflcl";
   18.34 -val rtrancl_subset = thm "rtrancl_subset";
   18.35 -val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl";
   18.36 -val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
   18.37 -val rtrancl_trans = thm "rtrancl_trans";
   18.38 -val tranclD = thm "tranclD";
   18.39 -val tranclE = thm "tranclE";
   18.40 -val trancl_converse = thm "trancl_converse";
   18.41 -val trancl_converseD = thm "trancl_converseD";
   18.42 -val trancl_converseI = thm "trancl_converseI";
   18.43 -val trancl_induct = thm "trancl_induct";
   18.44 -val trancl_insert = thm "trancl_insert";
   18.45 -val trancl_into_rtrancl = thm "trancl_into_rtrancl";
   18.46 -val trancl_into_trancl = thm "trancl_into_trancl";
   18.47 -val trancl_into_trancl2 = thm "trancl_into_trancl2";
   18.48 -val trancl_mono = thm "trancl_mono";
   18.49 -val trancl_subset_Sigma = thm "trancl_subset_Sigma";
   18.50 -val trancl_trans = thm "trancl_trans";
   18.51 -val trancl_trans_induct = thm "trancl_trans_induct";
   18.52 -val trans_rtrancl = thm "trans_rtrancl";
   18.53 -val trans_trancl = thm "trans_trancl";
    19.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Dec 05 22:14:53 2006 +0100
    19.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed Dec 06 01:12:36 2006 +0100
    19.3 @@ -288,6 +288,9 @@
    19.4    bij_image_Collect_eq
    19.5  
    19.6  ML {*
    19.7 +local
    19.8 +  val INT_D = thm "INT_D";
    19.9 +in
   19.10  (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
   19.11  fun list_of_Int th = 
   19.12      (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
   19.13 @@ -295,6 +298,7 @@
   19.14      handle THM _ => (list_of_Int (th RS INT_D))
   19.15      handle THM _ => (list_of_Int (th RS bspec))
   19.16      handle THM _ => [th];
   19.17 +end;
   19.18  *}
   19.19  
   19.20  lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
    20.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Tue Dec 05 22:14:53 2006 +0100
    20.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Wed Dec 06 01:12:36 2006 +0100
    20.3 @@ -7,6 +7,7 @@
    20.4  *)
    20.5  
    20.6  (*ListOrder*)
    20.7 +val Domain_def = thm "Domain_def";
    20.8  val Le_def = thm "Le_def";
    20.9  val Ge_def = thm "Ge_def";
   20.10  val prefix_def = thm "prefix_def";
    21.1 --- a/src/HOL/W0/W0.thy	Tue Dec 05 22:14:53 2006 +0100
    21.2 +++ b/src/HOL/W0/W0.thy	Wed Dec 06 01:12:36 2006 +0100
    21.3 @@ -353,7 +353,7 @@
    21.4    apply (tactic {*
    21.5      fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
    21.6      thm "free_tv_subst_var" RS subsetD]
    21.7 -    addss (simpset() delsimps bex_simps
    21.8 +    addss (simpset() delsimps (thms "bex_simps")
    21.9      addsimps [thm "cod_def", thm "dom_def"])) 1 *})
   21.10    done
   21.11  
   21.12 @@ -581,7 +581,7 @@
   21.13    apply (induct e)
   21.14      txt {* case @{text "Var n"} *}
   21.15      apply clarsimp
   21.16 -    apply (tactic {* fast_tac (HOL_cs addIs [nth_mem, subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
   21.17 +    apply (tactic {* fast_tac (HOL_cs addIs [thm "nth_mem", subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
   21.18     txt {* case @{text "Abs e"} *}
   21.19     apply (simp add: free_tv_subst split add: split_bind)
   21.20     apply (intro strip)
    22.1 --- a/src/HOL/ex/MT.ML	Tue Dec 05 22:14:53 2006 +0100
    22.2 +++ b/src/HOL/ex/MT.ML	Wed Dec 06 01:12:36 2006 +0100
    22.3 @@ -86,7 +86,7 @@
    22.4  by (assume_tac 1);
    22.5  by (blast_tac (claset() addSIs [cih]) 1);
    22.6  by (rtac (monoh RS monoD RS subsetD) 1);
    22.7 -by (rtac Un_upper2 1);
    22.8 +by (rtac (thm "Un_upper2") 1);
    22.9  by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
   22.10  qed "gfp_coind2";
   22.11  
   22.12 @@ -141,7 +141,7 @@
   22.13  
   22.14  (* Monotonicity of eval_fun *)
   22.15  
   22.16 -Goalw [mono_def, eval_fun_def] "mono(eval_fun)";
   22.17 +Goalw [thm "mono_def", eval_fun_def] "mono(eval_fun)";
   22.18  by infsys_mono_tac;
   22.19  qed "eval_fun_mono";
   22.20  
   22.21 @@ -259,7 +259,7 @@
   22.22  (* Elaborations                                                 *)
   22.23  (* ############################################################ *)
   22.24  
   22.25 -Goalw [mono_def, elab_fun_def] "mono(elab_fun)";
   22.26 +Goalw [thm "mono_def", elab_fun_def] "mono(elab_fun)";
   22.27  by infsys_mono_tac;
   22.28  qed "elab_fun_mono";
   22.29  
   22.30 @@ -480,7 +480,7 @@
   22.31  
   22.32  (* Monotonicity of hasty_fun *)
   22.33  
   22.34 -Goalw [mono_def, hasty_fun_def] "mono(hasty_fun)";
   22.35 +Goalw [thm "mono_def", hasty_fun_def] "mono(hasty_fun)";
   22.36  by infsys_mono_tac;
   22.37  by (Blast_tac 1);
   22.38  qed "mono_hasty_fun";
   22.39 @@ -607,7 +607,7 @@
   22.40  Goal "[| ve hastyenv te; v hasty t |] ==> \
   22.41  \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
   22.42  by (rewtac hasty_env_def);
   22.43 -by (asm_full_simp_tac (simpset() delsimps mem_simps
   22.44 +by (asm_full_simp_tac (simpset() delsimps thms "mem_simps"
   22.45                                  addsimps [ve_dom_owr, te_dom_owr]) 1);
   22.46  by (safe_tac HOL_cs);
   22.47  by (excluded_middle_tac "ev=x" 1);
   22.48 @@ -651,12 +651,12 @@
   22.49  by (etac elab_fn 1);
   22.50  by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);
   22.51  
   22.52 -by (asm_simp_tac (simpset() delsimps mem_simps addsimps [ve_dom_owr]) 1);
   22.53 +by (asm_simp_tac (simpset() delsimps thms "mem_simps" addsimps [ve_dom_owr]) 1);
   22.54  by (safe_tac HOL_cs);
   22.55  by (excluded_middle_tac "ev2=ev1a" 1);
   22.56  by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
   22.57  
   22.58 -by (asm_simp_tac (simpset() delsimps mem_simps
   22.59 +by (asm_simp_tac (simpset() delsimps thms "mem_simps"
   22.60                             addsimps [ve_app_owr1, te_app_owr1]) 1);
   22.61  by (Blast_tac 1);
   22.62  qed "consistency_fix";
    23.1 --- a/src/HOL/ex/reflection.ML	Tue Dec 05 22:14:53 2006 +0100
    23.2 +++ b/src/HOL/ex/reflection.ML	Wed Dec 06 01:12:36 2006 +0100
    23.3 @@ -14,6 +14,9 @@
    23.4  = struct
    23.5  
    23.6  val ext2 = thm "ext2";
    23.7 +val nth_Cons_0 = thm "nth_Cons_0";
    23.8 +val nth_Cons_Suc = thm "nth_Cons_Suc";
    23.9 +
   23.10    (* Make a congruence rule out of a defining equation for the interpretation *)
   23.11    (* th is one defining equation of f, i.e.
   23.12       th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)