--- a/src/HOL/Bali/AxCompl.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Bali/AxCompl.thy Wed Dec 06 01:12:36 2006 +0100
@@ -1406,7 +1406,7 @@
apply -
apply (induct_tac "n")
apply (tactic "ALLGOALS Clarsimp_tac")
-apply (tactic "dtac (permute_prems 0 1 card_seteq) 1")
+apply (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *})
apply simp
apply (erule finite_imageI)
apply (simp add: MGF_asm ax_derivs_asm)
--- a/src/HOL/Datatype.ML Tue Dec 05 22:14:53 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(* Title: HOL/Datatype.ML
- ID: $Id$
- Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
-*)
-
-(** legacy ML bindings **)
-
-structure bool =
-struct
- val distinct = thms "bool.distinct";
- val inject = thms "bool.inject";
- val exhaust = thm "bool.exhaust";
- val cases = thms "bool.cases";
- val split = thm "bool.split";
- val split_asm = thm "bool.split_asm";
- val induct = thm "bool.induct";
- val recs = thms "bool.recs";
- val simps = thms "bool.simps";
- val size = thms "bool.size";
-end;
-
-structure sum =
-struct
- val distinct = thms "sum.distinct";
- val inject = thms "sum.inject";
- val exhaust = thm "sum.exhaust";
- val cases = thms "sum.cases";
- val split = thm "sum.split";
- val split_asm = thm "sum.split_asm";
- val induct = thm "sum.induct";
- val recs = thms "sum.recs";
- val simps = thms "sum.simps";
- val size = thms "sum.size";
-end;
-
-structure unit =
-struct
- val distinct = thms "unit.distinct";
- val inject = thms "unit.inject";
- val exhaust = thm "unit.exhaust";
- val cases = thms "unit.cases";
- val split = thm "unit.split";
- val split_asm = thm "unit.split_asm";
- val induct = thm "unit.induct";
- val recs = thms "unit.recs";
- val simps = thms "unit.simps";
- val size = thms "unit.size";
-end;
-
-structure prod =
-struct
- val distinct = thms "prod.distinct";
- val inject = thms "prod.inject";
- val exhaust = thm "prod.exhaust";
- val cases = thms "prod.cases";
- val split = thm "prod.split";
- val split_asm = thm "prod.split_asm";
- val induct = thm "prod.induct";
- val recs = thms "prod.recs";
- val simps = thms "prod.simps";
- val size = thms "prod.size";
-end;
-
-structure option =
-struct
- val distinct = thms "option.distinct";
- val inject = thms "option.inject";
- val exhaust = thm "option.exhaust";
- val cases = thms "option.cases";
- val split = thm "option.split";
- val split_asm = thm "option.split_asm";
- val induct = thm "option.induct";
- val recs = thms "option.recs";
- val simps = thms "option.simps";
- val size = thms "option.size";
-end;
-
-val elem_o2s = thm "elem_o2s";
-val not_None_eq = thm "not_None_eq";
-val not_Some_eq = thm "not_Some_eq";
-val o2s_empty_eq = thm "o2s_empty_eq";
-val option_caseE = thm "option_caseE";
-val option_map_None = thm "option_map_None";
-val option_map_Some = thm "option_map_Some";
-val option_map_def = thm "option_map_def";
-val option_map_eq_Some = thm "option_map_eq_Some";
-val option_map_o_sum_case = thm "option_map_o_sum_case";
-val ospec = thm "ospec";
-val sum_case_inject = thm "sum_case_inject";
-val sum_case_weak_cong = thm "sum_case_weak_cong";
-val surjective_sum = thm "surjective_sum";
--- a/src/HOL/Datatype.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Datatype.thy Wed Dec 06 01:12:36 2006 +0100
@@ -6,7 +6,7 @@
Could <*> be generalized to a general summation (Sigma)?
*)
-header{*Analogues of the Cartesian Product and Disjoint Sum for Datatypes*}
+header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
theory Datatype
imports Nat Sum_Type
@@ -808,95 +808,12 @@
code_reserved Haskell
Bool True False not Maybe Nothing Just
-ML
-{*
-val apfst_conv = thm "apfst_conv";
-val apfst_convE = thm "apfst_convE";
-val Push_inject1 = thm "Push_inject1";
-val Push_inject2 = thm "Push_inject2";
-val Push_inject = thm "Push_inject";
-val Push_neq_K0 = thm "Push_neq_K0";
-val Abs_Node_inj = thm "Abs_Node_inj";
-val Node_K0_I = thm "Node_K0_I";
-val Node_Push_I = thm "Node_Push_I";
-val Scons_not_Atom = thm "Scons_not_Atom";
-val Atom_not_Scons = thm "Atom_not_Scons";
-val inj_Atom = thm "inj_Atom";
-val Atom_inject = thm "Atom_inject";
-val Atom_Atom_eq = thm "Atom_Atom_eq";
-val inj_Leaf = thm "inj_Leaf";
-val Leaf_inject = thm "Leaf_inject";
-val inj_Numb = thm "inj_Numb";
-val Numb_inject = thm "Numb_inject";
-val Push_Node_inject = thm "Push_Node_inject";
-val Scons_inject1 = thm "Scons_inject1";
-val Scons_inject2 = thm "Scons_inject2";
-val Scons_inject = thm "Scons_inject";
-val Scons_Scons_eq = thm "Scons_Scons_eq";
-val Scons_not_Leaf = thm "Scons_not_Leaf";
-val Leaf_not_Scons = thm "Leaf_not_Scons";
-val Scons_not_Numb = thm "Scons_not_Numb";
-val Numb_not_Scons = thm "Numb_not_Scons";
-val Leaf_not_Numb = thm "Leaf_not_Numb";
-val Numb_not_Leaf = thm "Numb_not_Leaf";
-val ndepth_K0 = thm "ndepth_K0";
-val ndepth_Push_Node_aux = thm "ndepth_Push_Node_aux";
-val ndepth_Push_Node = thm "ndepth_Push_Node";
-val ntrunc_0 = thm "ntrunc_0";
-val ntrunc_Atom = thm "ntrunc_Atom";
-val ntrunc_Leaf = thm "ntrunc_Leaf";
-val ntrunc_Numb = thm "ntrunc_Numb";
-val ntrunc_Scons = thm "ntrunc_Scons";
-val ntrunc_one_In0 = thm "ntrunc_one_In0";
-val ntrunc_In0 = thm "ntrunc_In0";
-val ntrunc_one_In1 = thm "ntrunc_one_In1";
-val ntrunc_In1 = thm "ntrunc_In1";
-val uprodI = thm "uprodI";
-val uprodE = thm "uprodE";
-val uprodE2 = thm "uprodE2";
-val usum_In0I = thm "usum_In0I";
-val usum_In1I = thm "usum_In1I";
-val usumE = thm "usumE";
-val In0_not_In1 = thm "In0_not_In1";
-val In1_not_In0 = thm "In1_not_In0";
-val In0_inject = thm "In0_inject";
-val In1_inject = thm "In1_inject";
-val In0_eq = thm "In0_eq";
-val In1_eq = thm "In1_eq";
-val inj_In0 = thm "inj_In0";
-val inj_In1 = thm "inj_In1";
-val Lim_inject = thm "Lim_inject";
-val ntrunc_subsetI = thm "ntrunc_subsetI";
-val ntrunc_subsetD = thm "ntrunc_subsetD";
-val ntrunc_equality = thm "ntrunc_equality";
-val ntrunc_o_equality = thm "ntrunc_o_equality";
-val uprod_mono = thm "uprod_mono";
-val usum_mono = thm "usum_mono";
-val Scons_mono = thm "Scons_mono";
-val In0_mono = thm "In0_mono";
-val In1_mono = thm "In1_mono";
-val Split = thm "Split";
-val Case_In0 = thm "Case_In0";
-val Case_In1 = thm "Case_In1";
-val ntrunc_UN1 = thm "ntrunc_UN1";
-val Scons_UN1_x = thm "Scons_UN1_x";
-val Scons_UN1_y = thm "Scons_UN1_y";
-val In0_UN1 = thm "In0_UN1";
-val In1_UN1 = thm "In1_UN1";
-val dprodI = thm "dprodI";
-val dprodE = thm "dprodE";
-val dsum_In0I = thm "dsum_In0I";
-val dsum_In1I = thm "dsum_In1I";
-val dsumE = thm "dsumE";
-val dprod_mono = thm "dprod_mono";
-val dsum_mono = thm "dsum_mono";
-val dprod_Sigma = thm "dprod_Sigma";
-val dprod_subset_Sigma = thm "dprod_subset_Sigma";
-val dprod_subset_Sigma2 = thm "dprod_subset_Sigma2";
-val dsum_Sigma = thm "dsum_Sigma";
-val dsum_subset_Sigma = thm "dsum_subset_Sigma";
-val Domain_dprod = thm "Domain_dprod";
-val Domain_dsum = thm "Domain_dsum";
+
+subsection {* Basic ML bindings *}
+
+ML {*
+val not_None_eq = thm "not_None_eq";
+val not_Some_eq = thm "not_Some_eq";
*}
end
--- a/src/HOL/Finite_Set.ML Tue Dec 05 22:14:53 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-
-(* legacy ML bindings *)
-
-structure Finites =
-struct
- val intrs = thms "Finites.intros";
- val elims = thms "Finites.cases";
- val elim = thm "Finites.cases";
- val induct = thm "Finites.induct";
- val mk_cases = OldInductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
- val [emptyI, insertI] = thms "Finites.intros";
-end;
-
-structure foldSet =
-struct
- val intrs = thms "foldSet.intros";
- val elims = thms "foldSet.cases";
- val elim = thm "foldSet.cases";
- val induct = thm "foldSet.induct";
- val mk_cases = OldInductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
- val [emptyI, insertI] = thms "foldSet.intros";
-end;
-
-val card_0_eq = thm "card_0_eq";
-val card_Diff1_le = thm "card_Diff1_le";
-val card_Diff1_less = thm "card_Diff1_less";
-val card_Diff2_less = thm "card_Diff2_less";
-val card_Diff_singleton = thm "card_Diff_singleton";
-val card_Diff_singleton_if = thm "card_Diff_singleton_if";
-val card_Diff_subset = thm "card_Diff_subset";
-val card_Pow = thm "card_Pow";
-val card_Suc_Diff1 = thm "card_Suc_Diff1";
-val card_Un_Int = thm "card_Un_Int";
-val card_Un_disjoint = thm "card_Un_disjoint";
-val card_bij_eq = thm "card_bij_eq";
-val card_def = thm "card_def";
-val card_empty = thm "card_empty";
-val card_eq_setsum = thm "card_eq_setsum";
-val card_image = thm "card_image";
-val card_image_le = thm "card_image_le";
-val card_inj_on_le = thm "card_inj_on_le";
-val card_insert = thm "card_insert";
-val card_insert_disjoint = thm "card_insert_disjoint";
-val card_insert_if = thm "card_insert_if";
-val card_insert_le = thm "card_insert_le";
-val card_mono = thm "card_mono";
-val card_psubset = thm "card_psubset";
-val card_seteq = thm "card_seteq";
-val Diff1_foldSet = thm "Diff1_foldSet";
-val dvd_partition = thm "dvd_partition";
-val empty_foldSetE = thm "empty_foldSetE";
-val endo_inj_surj = thm "endo_inj_surj";
-val finite = thm "finite";
-val finite_Diff = thm "finite_Diff";
-val finite_Diff_insert = thm "finite_Diff_insert";
-val finite_Field = thm "finite_Field";
-val finite_imp_foldSet = thm "finite_imp_foldSet";
-val finite_Int = thm "finite_Int";
-val finite_Pow_iff = thm "finite_Pow_iff";
-val finite_Prod_UNIV = thm "finite_Prod_UNIV";
-val finite_SigmaI = thm "finite_SigmaI";
-val finite_UN = thm "finite_UN";
-val finite_UN_I = thm "finite_UN_I";
-val finite_Un = thm "finite_Un";
-val finite_UnI = thm "finite_UnI";
-val finite_converse = thm "finite_converse";
-val finite_empty_induct = thm "finite_empty_induct";
-val finite_imageD = thm "finite_imageD";
-val finite_imageI = thm "finite_imageI";
-val finite_induct = thm "finite_induct";
-val finite_insert = thm "finite_insert";
-val finite_range_imageI = thm "finite_range_imageI";
-val finite_subset = thm "finite_subset";
-val finite_subset_induct = thm "finite_subset_induct";
-val finite_trancl = thm "finite_trancl";
-val foldSet_determ = thm "ACf.foldSet_determ";
-val foldSet_imp_finite = thm "foldSet_imp_finite";
-val fold_Un_Int = thm "ACe.fold_Un_Int";
-val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
-val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint";
-val fold_commute = thm "ACf.fold_commute";
-val fold_def = thm "fold_def";
-val fold_empty = thm "fold_empty";
-val fold_equality = thm "ACf.fold_equality";
-val fold_insert = thm "ACf.fold_insert";
-val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int";
-val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint";
-val psubset_card_mono = thm "psubset_card_mono";
-val setsum_0 = thm "setsum_0";
-val setsum_SucD = thm "setsum_SucD";
-val setsum_UN_disjoint = thm "setsum_UN_disjoint";
-val setsum_Un = thm "setsum_Un";
-val setsum_Un_Int = thm "setsum_Un_Int";
-val setsum_Un_disjoint = thm "setsum_Un_disjoint";
-val setsum_addf = thm "setsum_addf";
-val setsum_cong = thm "setsum_cong";
-val setsum_def = thm "setsum_def";
-val setsum_diff1 = thm "setsum_diff1";
-val setsum_empty = thm "setsum_empty";
-val setsum_eq_0_iff = thm "setsum_eq_0_iff";
-val setsum_insert = thm "setsum_insert";
-val trancl_subset_Field2 = thm "trancl_subset_Field2";
--- a/src/HOL/HoareParallel/Gar_Coll.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/HoareParallel/Gar_Coll.thy Wed Dec 06 01:12:36 2006 +0100
@@ -798,7 +798,7 @@
apply simp_all
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
done
subsubsection {* Interference freedom Mutator-Collector *}
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Wed Dec 06 01:12:36 2006 +0100
@@ -1211,15 +1211,15 @@
apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
apply(simp_all add:Graph10)
--{* 47 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
--{* 41 subgoals left *}
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"])]) *})
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
--{* 31 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
--{* 29 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
--{* 25 subgoals left *}
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"])]) *})
--{* 10 subgoals left *}
--- a/src/HOL/IsaMakefile Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/IsaMakefile Wed Dec 06 01:12:36 2006 +0100
@@ -84,9 +84,8 @@
$(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML \
$(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
Tools/res_atpset.ML \
- Code_Generator.thy Datatype.ML Datatype.thy \
- Divides.thy \
- Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
+ Code_Generator.thy Datatype.thy Divides.thy \
+ Equiv_Relations.thy Extraction.thy Finite_Set.thy \
FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy \
Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy \
Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy \
@@ -94,11 +93,10 @@
Integ/cooper_proof.ML Integ/reflected_presburger.ML \
Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML \
Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy \
- Lattices.thy List.ML List.thy Main.thy Map.thy \
- Nat.ML Nat.thy OrderedGroup.ML OrderedGroup.thy \
- Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy \
+ Lattices.thy List.thy Main.thy Map.thy Nat.thy Nat.ML OrderedGroup.ML \
+ OrderedGroup.thy Orderings.thy Power.thy PreList.thy Product_Type.thy \
ROOT.ML Recdef.thy Record.thy Refute.thy \
- Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML \
+ Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy \
Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML \
Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \
Tools/cnf_funcs.ML \
@@ -117,9 +115,8 @@
Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML \
Tools/typecopy_package.ML \
Tools/typedef_package.ML Tools/typedef_codegen.ML \
- Transitive_Closure.ML Transitive_Closure.thy \
- Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy \
- arith_data.ML \
+ Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \
+ Wellfounded_Relations.thy arith_data.ML \
document/root.tex hologic.ML simpdata.ML ATP_Linkup.thy \
Tools/res_atp_provers.ML Tools/res_atp_methods.ML \
Tools/res_hol_clause.ML \
--- a/src/HOL/Lambda/Commutation.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Lambda/Commutation.thy Wed Dec 06 01:12:36 2006 +0100
@@ -130,8 +130,9 @@
apply (tactic {* safe_tac HOL_cs *})
apply (tactic {*
blast_tac (HOL_cs addIs
- [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
- rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
+ [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans",
+ thm "rtrancl_converseI", thm "converseI",
+ thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *})
apply (erule rtrancl_induct)
apply blast
apply (blast del: rtrancl_refl intro: rtrancl_trans)
--- a/src/HOL/List.ML Tue Dec 05 22:14:53 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,231 +0,0 @@
-
-(** legacy ML bindings **)
-
-val Cons_eq_appendI = thm "Cons_eq_appendI";
-val Cons_in_lex = thm "Cons_in_lex";
-val Nil2_notin_lex = thm "Nil2_notin_lex";
-val Nil_eq_concat_conv = thm "Nil_eq_concat_conv";
-val Nil_is_append_conv = thm "Nil_is_append_conv";
-val Nil_is_map_conv = thm "Nil_is_map_conv";
-val Nil_is_rev_conv = thm "Nil_is_rev_conv";
-val Nil_notin_lex = thm "Nil_notin_lex";
-val all_nth_imp_all_set = thm "all_nth_imp_all_set";
-val all_set_conv_all_nth = thm "all_set_conv_all_nth";
-val append1_eq_conv = thm "append1_eq_conv";
-val append_Cons = thm "append_Cons";
-val append_Nil = thm "append_Nil";
-val append_Nil2 = thm "append_Nil2";
-val append_assoc = thm "append_assoc";
-val append_butlast_last_id = thm "append_butlast_last_id";
-val append_eq_appendI = thm "append_eq_appendI";
-val append_eq_append_conv = thm "append_eq_append_conv";
-val append_eq_conv_conj = thm "append_eq_conv_conj";
-val append_in_lists_conv = thm "append_in_lists_conv";
-val append_is_Nil_conv = thm "append_is_Nil_conv";
-val append_same_eq = thm "append_same_eq";
-val append_self_conv = thm "append_self_conv";
-val append_self_conv2 = thm "append_self_conv2";
-val append_take_drop_id = thm "append_take_drop_id";
-val butlast_append = thm "butlast_append";
-val butlast_snoc = thm "butlast_snoc";
-val concat_append = thm "concat_append";
-val concat_eq_Nil_conv = thm "concat_eq_Nil_conv";
-val distinct_append = thm "distinct_append";
-val distinct_filter = thm "distinct_filter";
-val distinct_remdups = thm "distinct_remdups";
-val dropWhile_append1 = thm "dropWhile_append1";
-val dropWhile_append2 = thm "dropWhile_append2";
-val drop_0 = thm "drop_0";
-val drop_Cons = thm "drop_Cons";
-val drop_Cons' = thm "drop_Cons'";
-val drop_Nil = thm "drop_Nil";
-val drop_Suc_Cons = thm "drop_Suc_Cons";
-val drop_all = thm "drop_all";
-val drop_append = thm "drop_append";
-val drop_drop = thm "drop_drop";
-val drop_map = thm "drop_map";
-val elem_le_sum = thm "elem_le_sum";
-val eq_Nil_appendI = thm "eq_Nil_appendI";
-val filter_False = thm "filter_False";
-val filter_True = thm "filter_True";
-val filter_append = thm "filter_append";
-val filter_concat = thm "filter_concat";
-val filter_filter = thm "filter_filter";
-val filter_is_subset = thm "filter_is_subset";
-val finite_set = thm "finite_set";
-val foldl_Cons = thm "foldl_Cons";
-val foldl_Nil = thm "foldl_Nil";
-val foldl_append = thm "foldl_append";
-val hd_Cons_tl = thm "hd_Cons_tl";
-val hd_append = thm "hd_append";
-val hd_append2 = thm "hd_append2";
-val hd_replicate = thm "hd_replicate";
-val in_listsD = thm "in_listsD";
-val in_listsI = thm "in_listsI";
-val in_lists_conv_set = thm "in_lists_conv_set";
-val in_set_butlastD = thm "in_set_butlastD";
-val in_set_butlast_appendI = thm "in_set_butlast_appendI";
-val in_set_conv_decomp = thm "in_set_conv_decomp";
-val in_set_replicateD = thm "in_set_replicateD";
-val inj_map = thm "inj_map";
-val inj_mapD = thm "inj_mapD";
-val inj_mapI = thm "inj_mapI";
-val last_replicate = thm "last_replicate";
-val last_snoc = thm "last_snoc";
-val length_0_conv = thm "length_0_conv";
-val length_Suc_conv = thm "length_Suc_conv";
-val length_append = thm "length_append";
-val length_butlast = thm "length_butlast";
-val length_drop = thm "length_drop";
-val length_filter_le = thm "length_filter_le";
-val length_greater_0_conv = thm "length_greater_0_conv";
-val length_induct = thm "length_induct";
-val length_list_update = thm "length_list_update";
-val length_map = thm "length_map";
-val length_replicate = thm "length_replicate";
-val length_rev = thm "length_rev";
-val length_take = thm "length_take";
-val length_tl = thm "length_tl";
-val length_upt = thm "length_upt";
-val length_zip = thm "length_zip";
-val lex_conv = thm "lex_conv";
-val lex_def = thm "lex_def";
-val lenlex_conv = thm "lenlex_conv";
-val lenlex_def = thm "lenlex_def";
-val lexn_conv = thm "lexn_conv";
-val lexn_length = thm "lexn_length";
-val list_all2_Cons = thm "list_all2_Cons";
-val list_all2_Cons1 = thm "list_all2_Cons1";
-val list_all2_Cons2 = thm "list_all2_Cons2";
-val list_all2_Nil = thm "list_all2_Nil";
-val list_all2_Nil2 = thm "list_all2_Nil2";
-val list_all2_append1 = thm "list_all2_append1";
-val list_all2_append2 = thm "list_all2_append2";
-val list_all2_conv_all_nth = thm "list_all2_conv_all_nth";
-val list_all2_def = thm "list_all2_def";
-val list_all2_lengthD = thm "list_all2_lengthD";
-val list_all2_rev = thm "list_all2_rev";
-val list_all2_trans = thm "list_all2_trans";
-val list_all_append = thm "list_all_append";
-val list_all_iff = thm "list_all_iff";
-val list_ball_nth = thm "list_ball_nth";
-val list_update_overwrite = thm "list_update_overwrite";
-val list_update_same_conv = thm "list_update_same_conv";
-val listsE = thm "listsE";
-val lists_IntI = thm "lists_IntI";
-val lists_Int_eq = thm "lists_Int_eq";
-val lists_mono = thm "lists_mono";
-val map_Suc_upt = thm "map_Suc_upt";
-val map_append = thm "map_append";
-val map_compose = thm "map_compose";
-val map_concat = thm "map_concat";
-val map_cong = thm "map_cong";
-val map_eq_Cons_conv = thm "map_eq_Cons_conv";
-val map_ext = thm "map_ext";
-val map_ident = thm "map_ident";
-val map_injective = thm "map_injective";
-val map_is_Nil_conv = thm "map_is_Nil_conv";
-val map_replicate = thm "map_replicate";
-val neq_Nil_conv = thm "neq_Nil_conv";
-val not_Cons_self = thm "not_Cons_self";
-val not_Cons_self2 = thm "not_Cons_self2";
-val nth_Cons = thm "nth_Cons";
-val nth_Cons' = thm "nth_Cons'";
-val nth_Cons_0 = thm "nth_Cons_0";
-val nth_Cons_Suc = thm "nth_Cons_Suc";
-val nth_append = thm "nth_append";
-val nth_drop = thm "nth_drop";
-val nth_equalityI = thm "nth_equalityI";
-val nth_list_update = thm "nth_list_update";
-val nth_list_update_eq = thm "nth_list_update_eq";
-val nth_list_update_neq = thm "nth_list_update_neq";
-val nth_map_upt = thm "nth_map_upt";
-val nth_mem = thm "nth_mem";
-val nth_replicate = thm "nth_replicate";
-val nth_take = thm "nth_take";
-val nth_take_lemma = thm "nth_take_lemma";
-val nth_upt = thm "nth_upt";
-val nth_zip = thm "nth_zip";
-val replicate_0 = thm "replicate_0";
-val replicate_Suc = thm "replicate_Suc";
-val replicate_add = thm "replicate_add";
-val replicate_app_Cons_same = thm "replicate_app_Cons_same";
-val rev_append = thm "rev_append";
-val rev_concat = thm "rev_concat";
-val rev_drop = thm "rev_drop";
-val rev_exhaust = thm "rev_exhaust";
-val rev_induct = thm "rev_induct";
-val rev_is_Nil_conv = thm "rev_is_Nil_conv";
-val rev_is_rev_conv = thm "rev_is_rev_conv";
-val rev_map = thm "rev_map";
-val rev_replicate = thm "rev_replicate";
-val rev_rev_ident = thm "rev_rev_ident";
-val rev_take = thm "rev_take";
-val same_append_eq = thm "same_append_eq";
-val self_append_conv = thm "self_append_conv";
-val self_append_conv2 = thm "self_append_conv2";
-val set_append = thm "set_append";
-val set_concat = thm "set_concat";
-val set_conv_nth = thm "set_conv_nth";
-val set_empty = thm "set_empty";
-val set_filter = thm "set_filter";
-val set_map = thm "set_map";
-val mem_ii = thm "mem_iff";
-val set_remdups = thm "set_remdups";
-val set_replicate = thm "set_replicate";
-val set_replicate_conv_if = thm "set_replicate_conv_if";
-val set_rev = thm "set_rev";
-val set_subset_Cons = thm "set_subset_Cons";
-val set_take_whileD = thm "set_take_whileD";
-val set_update_subsetI = thm "set_update_subsetI";
-val set_update_subset_insert = thm "set_update_subset_insert";
-val set_upt = thm "set_upt";
-val set_zip = thm "set_zip";
-val start_le_sum = thm "start_le_sum";
-val sublist_Cons = thm "sublist_Cons";
-val sublist_append = thm "sublist_append";
-val sublist_def = thm "sublist_def";
-val sublist_empty = thm "sublist_empty";
-val sublist_nil = thm "sublist_nil";
-val sublist_shift_lemma = thm "sublist_shift_lemma";
-val sublist_singleton = thm "sublist_singleton";
-val sublist_upt_eq_take = thm "sublist_upt_eq_take";
-val sum_eq_0_conv = thm "sum_eq_0_conv";
-val takeWhile_append1 = thm "takeWhile_append1";
-val takeWhile_append2 = thm "takeWhile_append2";
-val takeWhile_dropWhile_id = thm "takeWhile_dropWhile_id";
-val takeWhile_tail = thm "takeWhile_tail";
-val take_0 = thm "take_0";
-val take_Cons = thm "take_Cons";
-val take_Cons' = thm "take_Cons'";
-val take_Nil = thm "take_Nil";
-val take_Suc_Cons = thm "take_Suc_Cons";
-val take_all = thm "take_all";
-val take_append = thm "take_append";
-val take_drop = thm "take_drop";
-val take_equalityI = thm "take_equalityI";
-val take_map = thm "take_map";
-val take_take = thm "take_take";
-val take_upt = thm "take_upt";
-val tl_append = thm "tl_append";
-val tl_append2 = thm "tl_append2";
-val tl_replicate = thm "tl_replicate";
-val update_zip = thm "update_zip";
-val upt_0 = thm "upt_0";
-val upt_Suc = thm "upt_Suc";
-val upt_Suc_append = thm "upt_Suc_append";
-val upt_add_eq_append = thm "upt_add_eq_append";
-val upt_conv_Cons = thm "upt_conv_Cons";
-val upt_conv_Nil = thm "upt_conv_Nil";
-val upt_rec = thm "upt_rec";
-val wf_lex = thm "wf_lex";
-val wf_lenlex = thm "wf_lenlex";
-val wf_lexn = thm "wf_lexn";
-val zip_Cons_Cons = thm "zip_Cons_Cons";
-val zip_Nil = thm "zip_Nil";
-val zip_append = thm "zip_append";
-val zip_append1 = thm "zip_append1";
-val zip_append2 = thm "zip_append2";
-val zip_replicate = thm "zip_replicate";
-val zip_rev = thm "zip_rev";
-val zip_update = thm "zip_update";
--- a/src/HOL/Nat.ML Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Nat.ML Wed Dec 06 01:12:36 2006 +0100
@@ -17,17 +17,6 @@
val simps = thms "nat.simps";
end;
-val [nat_rec_0, nat_rec_Suc] = thms "nat.recs";
-bind_thm ("nat_rec_0", nat_rec_0);
-bind_thm ("nat_rec_Suc", nat_rec_Suc);
-
-val [nat_case_0, nat_case_Suc] = thms "nat.cases";
-bind_thm ("nat_case_0", nat_case_0);
-bind_thm ("nat_case_Suc", nat_case_Suc);
-
-val leD = thm "leD"; (*Now defined in Orderings.thy*)
-val leI = thm "leI";
-
val Least_Suc = thm "Least_Suc";
val Least_Suc2 = thm "Least_Suc2";
val One_nat_def = thm "One_nat_def";
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Dec 06 01:12:36 2006 +0100
@@ -16,6 +16,10 @@
structure NominalAtoms : NOMINAL_ATOMS =
struct
+val Finites_emptyI = thm "Finites.emptyI";
+val Collect_const = thm "Collect_const";
+
+
(* data kind 'HOL/nominal' *)
structure NominalArgs =
@@ -477,7 +481,7 @@
rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
else
let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
- val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI];
+ val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites_emptyI];
in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
in
AxClass.prove_arity (qu_name,[],[qu_class]) proof thy'
@@ -614,7 +618,7 @@
let
val qu_class = Sign.full_name thy ("fs_"^ak_name);
val supp_def = thm "Nominal.supp_def";
- val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
+ val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites_emptyI,defn];
val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
in
AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
--- a/src/HOL/Nominal/nominal_package.ML Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Wed Dec 06 01:12:36 2006 +0100
@@ -18,6 +18,18 @@
structure NominalPackage : NOMINAL_PACKAGE =
struct
+val Finites_emptyI = thm "Finites.emptyI";
+val finite_Diff = thm "finite_Diff";
+val finite_Un = thm "finite_Un";
+val Un_iff = thm "Un_iff";
+val In0_eq = thm "In0_eq";
+val In1_eq = thm "In1_eq";
+val In0_not_In1 = thm "In0_not_In1";
+val In1_not_In0 = thm "In1_not_In0";
+val Un_assoc = thm "Un_assoc";
+val Collect_disj_eq = thm "Collect_disj_eq";
+val empty_def = thm "empty_def";
+
open DatatypeAux;
open NominalAtoms;
@@ -1004,7 +1016,7 @@
(fn _ =>
simp_tac (HOL_basic_ss addsimps (supp_def ::
Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
- symmetric empty_def :: Finites.emptyI :: simp_thms @
+ symmetric empty_def :: Finites_emptyI :: simp_thms @
abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
in
(supp_thm,
--- a/src/HOL/Nominal/nominal_permeq.ML Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed Dec 06 01:12:36 2006 +0100
@@ -48,6 +48,9 @@
structure NominalPermeq : NOMINAL_PERMEQ =
struct
+val Finites_emptyI = thm "Finites.emptyI";
+val finite_Un = thm "finite_Un";
+
(* pulls out dynamically a thm via the proof state *)
fun dynamic_thms st name = PureThy.get_thms (theory_of_thm st) (Name name);
fun dynamic_thm st name = PureThy.get_thm (theory_of_thm st) (Name name);
@@ -278,7 +281,7 @@
Logic.strip_assums_concl (hd (prems_of supports_rule'));
val supports_rule'' = Drule.cterm_instantiate
[(cert (head_of S), cert s')] supports_rule'
- val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites.emptyI]
+ val ss' = ss addsimps [supp_prod, supp_unit, finite_Un, Finites_emptyI]
in
(tactical ("guessing of the right supports-set",
EVERY [compose_tac (false, supports_rule'', 2) i,
@@ -316,7 +319,7 @@
val supports_fresh_rule'' = Drule.cterm_instantiate
[(cert (head_of S), cert s')] supports_fresh_rule'
val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
- val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI]
+ val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites_emptyI]
(* FIXME sometimes these rewrite rules are already in the ss, *)
(* which produces a warning *)
in
--- a/src/HOL/Orderings.ML Tue Dec 05 22:14:53 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* legacy ML bindings *)
-
-val order_less_irrefl = thm "order_less_irrefl";
-val linorder_not_less = thm "linorder_not_less";
-val linorder_not_le = thm "linorder_not_le";
-val linorder_neq_iff = thm "linorder_neq_iff";
-val linorder_neqE = thm "linorder_neqE";
-val order_refl = thm "order_refl";
-val order_trans = thm "order_trans";
-val order_antisym = thm "order_antisym";
-val mono_def = thm "mono_def";
-val monoI = thm "monoI";
-val monoD = thm "monoD";
-val max_less_iff_conj = thm "max_less_iff_conj";
-val min_less_iff_conj = thm "min_less_iff_conj";
-val split_min = thm "split_min";
-val split_max = thm "split_max";
--- a/src/HOL/Relation.ML Tue Dec 05 22:14:53 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-
-(* legacy ML bindings *)
-
-val DomainE = thm "DomainE";
-val DomainI = thm "DomainI";
-val Domain_Collect_split = thm "Domain_Collect_split";
-val Domain_Diff_subset = thm "Domain_Diff_subset";
-val Domain_Id = thm "Domain_Id";
-val Domain_Int_subset = thm "Domain_Int_subset";
-val Domain_Un_eq = thm "Domain_Un_eq";
-val Domain_Union = thm "Domain_Union";
-val Domain_def = thm "Domain_def";
-val Domain_diag = thm "Domain_diag";
-val Domain_empty = thm "Domain_empty";
-val Domain_iff = thm "Domain_iff";
-val Domain_insert = thm "Domain_insert";
-val Domain_mono = thm "Domain_mono";
-val Field_def = thm "Field_def";
-val IdE = thm "IdE";
-val IdI = thm "IdI";
-val Id_O_R = thm "Id_O_R";
-val Id_def = thm "Id_def";
-val ImageE = thm "ImageE";
-val ImageI = thm "ImageI";
-val Image_Collect_split = thm "Image_Collect_split";
-val Image_INT_subset = thm "Image_INT_subset";
-val Image_Id = thm "Image_Id";
-val Image_Int_subset = thm "Image_Int_subset";
-val Image_UN = thm "Image_UN";
-val Image_Un = thm "Image_Un";
-val Image_def = thm "Image_def";
-val Image_diag = thm "Image_diag";
-val Image_empty = thm "Image_empty";
-val Image_eq_UN = thm "Image_eq_UN";
-val Image_iff = thm "Image_iff";
-val Image_mono = thm "Image_mono";
-val Image_singleton = thm "Image_singleton";
-val Image_singleton_iff = thm "Image_singleton_iff";
-val Image_subset = thm "Image_subset";
-val Image_subset_eq = thm "Image_subset_eq";
-val O_assoc = thm "O_assoc";
-val R_O_Id = thm "R_O_Id";
-val RangeE = thm "RangeE";
-val RangeI = thm "RangeI";
-val Range_Collect_split = thm "Range_Collect_split";
-val Range_Diff_subset = thm "Range_Diff_subset";
-val Range_Id = thm "Range_Id";
-val Range_Int_subset = thm "Range_Int_subset";
-val Range_Un_eq = thm "Range_Un_eq";
-val Range_Union = thm "Range_Union";
-val Range_def = thm "Range_def";
-val Range_diag = thm "Range_diag";
-val Range_empty = thm "Range_empty";
-val Range_iff = thm "Range_iff";
-val Range_insert = thm "Range_insert";
-val antisymD = thm "antisymD";
-val antisymI = thm "antisymI";
-val antisym_Id = thm "antisym_Id";
-val antisym_converse = thm "antisym_converse";
-val antisym_def = thm "antisym_def";
-val converseD = thm "converseD";
-val converseE = thm "converseE";
-val converseI = thm "converseI";
-val converse_Id = thm "converse_Id";
-val converse_converse = thm "converse_converse";
-val converse_def = thm "converse_def";
-val converse_diag = thm "converse_diag";
-val converse_iff = thm "converse_iff";
-val converse_rel_comp = thm "converse_rel_comp";
-val diagE = thm "diagE";
-val diagI = thm "diagI";
-val diag_def = thm "diag_def";
-val diag_eqI = thm "diag_eqI";
-val diag_iff = thm "diag_iff";
-val diag_subset_Times = thm "diag_subset_Times";
-val inv_image_def = thm "inv_image_def";
-val pair_in_Id_conv = thm "pair_in_Id_conv";
-val reflD = thm "reflD";
-val reflI = thm "reflI";
-val refl_converse = thm "refl_converse";
-val refl_def = thm "refl_def";
-val reflexive_Id = thm "reflexive_Id";
-val rel_compE = thm "rel_compE";
-val rel_compEpair = thm "rel_compEpair";
-val rel_compI = thm "rel_compI";
-val rel_comp_def = thm "rel_comp_def";
-val rel_comp_mono = thm "rel_comp_mono";
-val rel_comp_subset_Sigma = thm "rel_comp_subset_Sigma";
-val rev_ImageI = thm "rev_ImageI";
-val single_valuedD = thm "single_valuedD";
-val single_valuedI = thm "single_valuedI";
-val single_valued_def = thm "single_valued_def";
-val sym_def = thm "sym_def";
-val transD = thm "transD";
-val transI = thm "transI";
-val trans_Id = thm "trans_Id";
-val trans_O_subset = thm "trans_O_subset";
-val trans_converse = thm "trans_converse";
-val trans_def = thm "trans_def";
-val trans_inv_image = thm "trans_inv_image";
--- a/src/HOL/Set.ML Tue Dec 05 22:14:53 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,433 +0,0 @@
-
-(* legacy ML bindings *)
-
-val Ball_def = thm "Ball_def";
-val Bex_def = thm "Bex_def";
-val CollectD = thm "CollectD";
-val CollectE = thm "CollectE";
-val CollectI = thm "CollectI";
-val Collect_all_eq = thm "Collect_all_eq";
-val Collect_ball_eq = thm "Collect_ball_eq";
-val Collect_bex_eq = thm "Collect_bex_eq";
-val Collect_cong = thm "Collect_cong";
-val Collect_conj_eq = thm "Collect_conj_eq";
-val Collect_const = thm "Collect_const";
-val Collect_disj_eq = thm "Collect_disj_eq";
-val Collect_empty_eq = thm "Collect_empty_eq";
-val Collect_ex_eq = thm "Collect_ex_eq";
-val Collect_mem_eq = thm "Collect_mem_eq";
-val Collect_mono = thm "Collect_mono";
-val Collect_neg_eq = thm "Collect_neg_eq";
-val ComplD = thm "ComplD";
-val ComplE = thm "ComplE";
-val ComplI = thm "ComplI";
-val Compl_Diff_eq = thm "Compl_Diff_eq";
-val Compl_INT = thm "Compl_INT";
-val Compl_Int = thm "Compl_Int";
-val Compl_UN = thm "Compl_UN";
-val Compl_UNIV_eq = thm "Compl_UNIV_eq";
-val Compl_Un = thm "Compl_Un";
-val Compl_anti_mono = thm "Compl_anti_mono";
-val Compl_def = thm "Compl_def";
-val Compl_disjoint = thm "Compl_disjoint";
-val Compl_disjoint2 = thm "Compl_disjoint2";
-val Compl_empty_eq = thm "Compl_empty_eq";
-val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff";
-val Compl_iff = thm "Compl_iff";
-val Compl_partition = thm "Compl_partition";
-val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff";
-val DiffD1 = thm "DiffD1";
-val DiffD2 = thm "DiffD2";
-val DiffE = thm "DiffE";
-val DiffI = thm "DiffI";
-val Diff_Compl = thm "Diff_Compl";
-val Diff_Int = thm "Diff_Int";
-val Diff_Int_distrib = thm "Diff_Int_distrib";
-val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
-val Diff_UNIV = thm "Diff_UNIV";
-val Diff_Un = thm "Diff_Un";
-val Diff_cancel = thm "Diff_cancel";
-val Diff_disjoint = thm "Diff_disjoint";
-val Diff_empty = thm "Diff_empty";
-val Diff_eq = thm "Diff_eq";
-val Diff_eq_empty_iff = thm "Diff_eq_empty_iff";
-val Diff_iff = thm "Diff_iff";
-val Diff_insert = thm "Diff_insert";
-val Diff_insert0 = thm "Diff_insert0";
-val Diff_insert2 = thm "Diff_insert2";
-val Diff_insert_absorb = thm "Diff_insert_absorb";
-val Diff_mono = thm "Diff_mono";
-val Diff_partition = thm "Diff_partition";
-val Diff_subset = thm "Diff_subset";
-val Diff_triv = thm "Diff_triv";
-val INTER_def = thm "INTER_def";
-val INT_D = thm "INT_D";
-val INT_E = thm "INT_E";
-val INT_I = thm "INT_I";
-val INT_Int_distrib = thm "INT_Int_distrib";
-val INT_Un = thm "INT_Un";
-val INT_absorb = thm "INT_absorb";
-val INT_anti_mono = thm "INT_anti_mono";
-val INT_bool_eq = thm "INT_bool_eq";
-val INT_cong = thm "INT_cong";
-val INT_constant = thm "INT_constant";
-val INT_empty = thm "INT_empty";
-val INT_eq = thm "INT_eq";
-val INT_greatest = thm "INT_greatest";
-val INT_iff = thm "INT_iff";
-val INT_insert = thm "INT_insert";
-val INT_insert_distrib = thm "INT_insert_distrib";
-val INT_lower = thm "INT_lower";
-val INT_simps = thms "INT_simps";
-val INT_subset_iff = thm "INT_subset_iff";
-val IntD1 = thm "IntD1";
-val IntD2 = thm "IntD2";
-val IntE = thm "IntE";
-val IntI = thm "IntI";
-val Int_Collect = thm "Int_Collect";
-val Int_Collect_mono = thm "Int_Collect_mono";
-val Int_Diff = thm "Int_Diff";
-val Int_Inter_image = thm "Int_Inter_image";
-val Int_UNIV = thm "Int_UNIV";
-val Int_UNIV_left = thm "Int_UNIV_left";
-val Int_UNIV_right = thm "Int_UNIV_right";
-val Int_UN_distrib = thm "Int_UN_distrib";
-val Int_UN_distrib2 = thm "Int_UN_distrib2";
-val Int_Un_distrib = thm "Int_Un_distrib";
-val Int_Un_distrib2 = thm "Int_Un_distrib2";
-val Int_Union = thm "Int_Union";
-val Int_Union2 = thm "Int_Union2";
-val Int_absorb = thm "Int_absorb";
-val Int_absorb1 = thm "Int_absorb1";
-val Int_absorb2 = thm "Int_absorb2";
-val Int_ac = thms "Int_ac";
-val Int_assoc = thm "Int_assoc";
-val Int_commute = thm "Int_commute";
-val Int_def = thm "Int_def";
-val Int_empty_left = thm "Int_empty_left";
-val Int_empty_right = thm "Int_empty_right";
-val Int_eq_Inter = thm "Int_eq_Inter";
-val Int_greatest = thm "Int_greatest";
-val Int_iff = thm "Int_iff";
-val Int_insert_left = thm "Int_insert_left";
-val Int_insert_right = thm "Int_insert_right";
-val Int_left_absorb = thm "Int_left_absorb";
-val Int_left_commute = thm "Int_left_commute";
-val Int_lower1 = thm "Int_lower1";
-val Int_lower2 = thm "Int_lower2";
-val Int_mono = thm "Int_mono";
-val Int_subset_iff = thm "Int_subset_iff";
-val InterD = thm "InterD";
-val InterE = thm "InterE";
-val InterI = thm "InterI";
-val Inter_UNIV = thm "Inter_UNIV";
-val Inter_Un_distrib = thm "Inter_Un_distrib";
-val Inter_Un_subset = thm "Inter_Un_subset";
-val Inter_anti_mono = thm "Inter_anti_mono";
-val Inter_def = thm "Inter_def";
-val Inter_empty = thm "Inter_empty";
-val Inter_greatest = thm "Inter_greatest";
-val Inter_iff = thm "Inter_iff";
-val Inter_image_eq = thm "Inter_image_eq";
-val Inter_insert = thm "Inter_insert";
-val Inter_lower = thm "Inter_lower";
-val PowD = thm "PowD";
-val PowI = thm "PowI";
-val Pow_Compl = thm "Pow_Compl";
-val Pow_INT_eq = thm "Pow_INT_eq";
-val Pow_Int_eq = thm "Pow_Int_eq";
-val Pow_UNIV = thm "Pow_UNIV";
-val Pow_bottom = thm "Pow_bottom";
-val Pow_def = thm "Pow_def";
-val Pow_empty = thm "Pow_empty";
-val Pow_iff = thm "Pow_iff";
-val Pow_insert = thm "Pow_insert";
-val Pow_mono = thm "Pow_mono";
-val Pow_top = thm "Pow_top";
-val UNION_def = thm "UNION_def";
-val UNIV_I = thm "UNIV_I";
-val UNIV_def = thm "UNIV_def";
-val UNIV_not_empty = thm "UNIV_not_empty";
-val UNIV_witness = thm "UNIV_witness";
-val UN_E = thm "UN_E";
-val UN_I = thm "UN_I";
-val UN_Pow_subset = thm "UN_Pow_subset";
-val UN_UN_flatten = thm "UN_UN_flatten";
-val UN_Un = thm "UN_Un";
-val UN_Un_distrib = thm "UN_Un_distrib";
-val UN_absorb = thm "UN_absorb";
-val UN_bool_eq = thm "UN_bool_eq";
-val UN_cong = thm "UN_cong";
-val UN_constant = thm "UN_constant";
-val UN_empty = thm "UN_empty";
-val UN_empty2 = thm "UN_empty2";
-val UN_eq = thm "UN_eq";
-val UN_iff = thm "UN_iff";
-val UN_insert = thm "UN_insert";
-val UN_insert_distrib = thm "UN_insert_distrib";
-val UN_least = thm "UN_least";
-val UN_mono = thm "UN_mono";
-val UN_simps = thms "UN_simps";
-val UN_singleton = thm "UN_singleton";
-val UN_subset_iff = thm "UN_subset_iff";
-val UN_upper = thm "UN_upper";
-val UnCI = thm "UnCI";
-val UnE = thm "UnE";
-val UnI1 = thm "UnI1";
-val UnI2 = thm "UnI2";
-val Un_Diff = thm "Un_Diff";
-val Un_Diff_Int = thm "Un_Diff_Int";
-val Un_Diff_cancel = thm "Un_Diff_cancel";
-val Un_Diff_cancel2 = thm "Un_Diff_cancel2";
-val Un_INT_distrib = thm "Un_INT_distrib";
-val Un_INT_distrib2 = thm "Un_INT_distrib2";
-val Un_Int_assoc_eq = thm "Un_Int_assoc_eq";
-val Un_Int_crazy = thm "Un_Int_crazy";
-val Un_Int_distrib = thm "Un_Int_distrib";
-val Un_Int_distrib2 = thm "Un_Int_distrib2";
-val Un_Inter = thm "Un_Inter";
-val Un_Pow_subset = thm "Un_Pow_subset";
-val Un_UNIV_left = thm "Un_UNIV_left";
-val Un_UNIV_right = thm "Un_UNIV_right";
-val Un_Union_image = thm "Un_Union_image";
-val Un_absorb = thm "Un_absorb";
-val Un_absorb1 = thm "Un_absorb1";
-val Un_absorb2 = thm "Un_absorb2";
-val Un_ac = thms "Un_ac";
-val Un_assoc = thm "Un_assoc";
-val Un_commute = thm "Un_commute";
-val Un_def = thm "Un_def";
-val Un_empty = thm "Un_empty";
-val Un_empty_left = thm "Un_empty_left";
-val Un_empty_right = thm "Un_empty_right";
-val Un_eq_UN = thm "Un_eq_UN";
-val Un_eq_Union = thm "Un_eq_Union";
-val Un_iff = thm "Un_iff";
-val Un_insert_left = thm "Un_insert_left";
-val Un_insert_right = thm "Un_insert_right";
-val Un_least = thm "Un_least";
-val Un_left_absorb = thm "Un_left_absorb";
-val Un_left_commute = thm "Un_left_commute";
-val Un_mono = thm "Un_mono";
-val Un_subset_iff = thm "Un_subset_iff";
-val Un_upper1 = thm "Un_upper1";
-val Un_upper2 = thm "Un_upper2";
-val UnionE = thm "UnionE";
-val UnionI = thm "UnionI";
-val Union_Int_subset = thm "Union_Int_subset";
-val Union_Pow_eq = thm "Union_Pow_eq";
-val Union_UNIV = thm "Union_UNIV";
-val Union_Un_distrib = thm "Union_Un_distrib";
-val Union_def = thm "Union_def";
-val Union_disjoint = thm "Union_disjoint";
-val Union_empty = thm "Union_empty";
-val Union_empty_conv = thm "Union_empty_conv";
-val Union_iff = thm "Union_iff";
-val Union_image_eq = thm "Union_image_eq";
-val Union_insert = thm "Union_insert";
-val Union_least = thm "Union_least";
-val Union_mono = thm "Union_mono";
-val Union_upper = thm "Union_upper";
-val all_bool_eq = thm "all_bool_eq";
-val all_mono = thm "all_mono";
-val all_not_in_conv = thm "all_not_in_conv";
-val atomize_ball = thm "atomize_ball";
-val ballE = thm "ballE";
-val ballI = thm "ballI";
-val ball_UN = thm "ball_UN";
-val ball_UNIV = thm "ball_UNIV";
-val ball_Un = thm "ball_Un";
-val ball_cong = thm "ball_cong";
-val ball_conj_distrib = thm "ball_conj_distrib";
-val ball_empty = thm "ball_empty";
-val ball_one_point1 = thm "ball_one_point1";
-val ball_one_point2 = thm "ball_one_point2";
-val ball_simps = thms "ball_simps";
-val ball_triv = thm "ball_triv";
-val basic_monos = thms "basic_monos";
-val bexCI = thm "bexCI";
-val bexE = thm "bexE";
-val bexI = thm "bexI";
-val bex_UN = thm "bex_UN";
-val bex_UNIV = thm "bex_UNIV";
-val bex_Un = thm "bex_Un";
-val bex_cong = thm "bex_cong";
-val bex_disj_distrib = thm "bex_disj_distrib";
-val bex_empty = thm "bex_empty";
-val bex_one_point1 = thm "bex_one_point1";
-val bex_one_point2 = thm "bex_one_point2";
-val bex_simps = thms "bex_simps";
-val bex_triv = thm "bex_triv";
-val bex_triv_one_point1 = thm "bex_triv_one_point1";
-val bex_triv_one_point2 = thm "bex_triv_one_point2";
-val bool_induct = thm "bool_induct";
-val bspec = thm "bspec";
-val conj_mono = thm "conj_mono";
-val contra_subsetD = thm "contra_subsetD";
-val diff_single_insert = thm "diff_single_insert";
-val disj_mono = thm "disj_mono";
-val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl";
-val disjoint_iff_not_equal = thm "disjoint_iff_not_equal";
-val distinct_lemma = thm "distinct_lemma";
-val double_complement = thm "double_complement";
-val double_diff = thm "double_diff";
-val emptyE = thm "emptyE";
-val empty_Diff = thm "empty_Diff";
-val empty_def = thm "empty_def";
-val empty_iff = thm "empty_iff";
-val empty_subsetI = thm "empty_subsetI";
-val eq_to_mono = thm "eq_to_mono";
-val eq_to_mono2 = thm "eq_to_mono2";
-val eqset_imp_iff = thm "eqset_imp_iff";
-val equalityCE = thm "equalityCE";
-val equalityD1 = thm "equalityD1";
-val equalityD2 = thm "equalityD2";
-val equalityE = thm "equalityE";
-val equalityI = thm "equalityI";
-val equals0D = thm "equals0D";
-val equals0I = thm "equals0I";
-val ex_bool_eq = thm "ex_bool_eq";
-val ex_mono = thm "ex_mono";
-val full_SetCompr_eq = thm "full_SetCompr_eq";
-val if_image_distrib = thm "if_image_distrib";
-val imageE = thm "imageE";
-val imageI = thm "imageI";
-val image_Collect = thm "image_Collect";
-val image_Un = thm "image_Un";
-val image_Union = thm "image_Union";
-val image_cong = thm "image_cong";
-val image_constant = thm "image_constant";
-val image_def = thm "image_def";
-val image_empty = thm "image_empty";
-val image_eqI = thm "image_eqI";
-val image_iff = thm "image_iff";
-val image_image = thm "image_image";
-val image_insert = thm "image_insert";
-val image_is_empty = thm "image_is_empty";
-val image_mono = thm "image_mono";
-val image_subsetI = thm "image_subsetI";
-val image_subset_iff = thm "image_subset_iff";
-val imp_mono = thm "imp_mono";
-val imp_refl = thm "imp_refl";
-val in_mono = thm "in_mono";
-val insertCI = thm "insertCI";
-val insertE = thm "insertE";
-val insertI1 = thm "insertI1";
-val insertI2 = thm "insertI2";
-val insert_Collect = thm "insert_Collect";
-val insert_Diff = thm "insert_Diff";
-val insert_Diff1 = thm "insert_Diff1";
-val insert_Diff_if = thm "insert_Diff_if";
-val insert_absorb = thm "insert_absorb";
-val insert_absorb2 = thm "insert_absorb2";
-val insert_commute = thm "insert_commute";
-val insert_def = thm "insert_def";
-val insert_iff = thm "insert_iff";
-val insert_image = thm "insert_image";
-val insert_is_Un = thm "insert_is_Un";
-val insert_mono = thm "insert_mono";
-val insert_not_empty = thm "insert_not_empty";
-val insert_subset = thm "insert_subset";
-val mem_Collect_eq = thm "mem_Collect_eq";
-val mem_simps = thms "mem_simps";
-val mk_disjoint_insert = thm "mk_disjoint_insert";
-val mono_Int = thm "mono_Int";
-val mono_Un = thm "mono_Un";
-val not_psubset_empty = thm "not_psubset_empty";
-val psubsetI = thm "psubsetI";
-val psubset_def = thm "psubset_def";
-val psubset_eq = thm "psubset_eq";
-val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
-val psubset_imp_subset = thm "psubset_imp_subset";
-val psubset_insert_iff = thm "psubset_insert_iff";
-val psubset_subset_trans = thm "psubset_subset_trans";
-val rangeE = thm "rangeE";
-val rangeI = thm "rangeI";
-val range_composition = thm "range_composition";
-val range_eqI = thm "range_eqI";
-val rev_bexI = thm "rev_bexI";
-val rev_image_eqI = thm "rev_image_eqI";
-val rev_subsetD = thm "rev_subsetD";
-val set_diff_def = thm "set_diff_def";
-val set_eq_subset = thm "set_eq_subset";
-val set_ext = thm "set_ext";
-val singletonD = thm "singletonD";
-val singletonE = thm "singletonE";
-val singletonI = thm "singletonI";
-val singleton_conv = thm "singleton_conv";
-val singleton_conv2 = thm "singleton_conv2";
-val singleton_iff = thm "singleton_iff";
-val singleton_inject = thm "singleton_inject";
-val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
-val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
-val split_if_eq1 = thm "split_if_eq1";
-val split_if_eq2 = thm "split_if_eq2";
-val split_if_mem1 = thm "split_if_mem1";
-val split_if_mem2 = thm "split_if_mem2";
-val split_ifs = thms "split_ifs";
-val strip = thms "strip";
-val subsetCE = thm "subsetCE";
-val subsetD = thm "subsetD";
-val subsetI = thm "subsetI";
-val subset_Compl_self_eq = thm "subset_Compl_self_eq";
-val subset_Pow_Union = thm "subset_Pow_Union";
-val subset_UNIV = thm "subset_UNIV";
-val subset_Un_eq = thm "subset_Un_eq";
-val subset_antisym = thm "subset_antisym";
-val subset_def = thm "subset_def";
-val subset_empty = thm "subset_empty";
-val subset_iff = thm "subset_iff";
-val subset_iff_psubset_eq = thm "subset_iff_psubset_eq";
-val subset_image_iff = thm "subset_image_iff";
-val subset_insert = thm "subset_insert";
-val subset_insertI = thm "subset_insertI";
-val subset_insert_iff = thm "subset_insert_iff";
-val subset_psubset_trans = thm "subset_psubset_trans";
-val subset_refl = thm "subset_refl";
-val subset_singletonD = thm "subset_singletonD";
-val subset_trans = thm "subset_trans";
-val vimageD = thm "vimageD";
-val vimageE = thm "vimageE";
-val vimageI = thm "vimageI";
-val vimageI2 = thm "vimageI2";
-val vimage_Collect = thm "vimage_Collect";
-val vimage_Collect_eq = thm "vimage_Collect_eq";
-val vimage_Compl = thm "vimage_Compl";
-val vimage_Diff = thm "vimage_Diff";
-val vimage_INT = thm "vimage_INT";
-val vimage_Int = thm "vimage_Int";
-val vimage_UN = thm "vimage_UN";
-val vimage_UNIV = thm "vimage_UNIV";
-val vimage_Un = thm "vimage_Un";
-val vimage_Union = thm "vimage_Union";
-val vimage_def = thm "vimage_def";
-val vimage_empty = thm "vimage_empty";
-val vimage_eq = thm "vimage_eq";
-val vimage_eq_UN = thm "vimage_eq_UN";
-val vimage_insert = thm "vimage_insert";
-val vimage_mono = thm "vimage_mono";
-val vimage_singleton_eq = thm "vimage_singleton_eq";
-
-structure Set =
-struct
- val thy = the_context ();
- val Ball_def = Ball_def;
- val Bex_def = Bex_def;
- val Collect_mem_eq = Collect_mem_eq;
- val Compl_def = Compl_def;
- val INTER_def = INTER_def;
- val Int_def = Int_def;
- val Inter_def = Inter_def;
- val Pow_def = Pow_def;
- val UNION_def = UNION_def;
- val UNIV_def = UNIV_def;
- val Un_def = Un_def;
- val Union_def = Union_def;
- val empty_def = empty_def;
- val image_def = image_def;
- val insert_def = insert_def;
- val mem_Collect_eq = mem_Collect_eq;
- val psubset_def = psubset_def;
- val set_diff_def = set_diff_def;
- val subset_def = subset_def;
-end;
--- a/src/HOL/Set.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/Set.thy Wed Dec 06 01:12:36 2006 +0100
@@ -2110,4 +2110,65 @@
lemmas basic_trans_rules [trans] =
order_trans_rules set_rev_mp set_mp
+
+subsection {* Basic ML bindings *}
+
+ML {*
+val Ball_def = thm "Ball_def";
+val Bex_def = thm "Bex_def";
+val CollectD = thm "CollectD";
+val CollectE = thm "CollectE";
+val CollectI = thm "CollectI";
+val Collect_conj_eq = thm "Collect_conj_eq";
+val Collect_mem_eq = thm "Collect_mem_eq";
+val IntD1 = thm "IntD1";
+val IntD2 = thm "IntD2";
+val IntE = thm "IntE";
+val IntI = thm "IntI";
+val Int_Collect = thm "Int_Collect";
+val UNIV_I = thm "UNIV_I";
+val UNIV_witness = thm "UNIV_witness";
+val UnE = thm "UnE";
+val UnI1 = thm "UnI1";
+val UnI2 = thm "UnI2";
+val ballE = thm "ballE";
+val ballI = thm "ballI";
+val bexCI = thm "bexCI";
+val bexE = thm "bexE";
+val bexI = thm "bexI";
+val bex_triv = thm "bex_triv";
+val bspec = thm "bspec";
+val contra_subsetD = thm "contra_subsetD";
+val distinct_lemma = thm "distinct_lemma";
+val eq_to_mono = thm "eq_to_mono";
+val eq_to_mono2 = thm "eq_to_mono2";
+val equalityCE = thm "equalityCE";
+val equalityD1 = thm "equalityD1";
+val equalityD2 = thm "equalityD2";
+val equalityE = thm "equalityE";
+val equalityI = thm "equalityI";
+val imageE = thm "imageE";
+val imageI = thm "imageI";
+val image_Un = thm "image_Un";
+val image_insert = thm "image_insert";
+val insert_commute = thm "insert_commute";
+val insert_iff = thm "insert_iff";
+val mem_Collect_eq = thm "mem_Collect_eq";
+val rangeE = thm "rangeE";
+val rangeI = thm "rangeI";
+val range_eqI = thm "range_eqI";
+val subsetCE = thm "subsetCE";
+val subsetD = thm "subsetD";
+val subsetI = thm "subsetI";
+val subset_refl = thm "subset_refl";
+val subset_trans = thm "subset_trans";
+val vimageD = thm "vimageD";
+val vimageE = thm "vimageE";
+val vimageI = thm "vimageI";
+val vimageI2 = thm "vimageI2";
+val vimage_Collect = thm "vimage_Collect";
+val vimage_Int = thm "vimage_Int";
+val vimage_Un = thm "vimage_Un";
+*}
+
end
--- a/src/HOL/Transitive_Closure.ML Tue Dec 05 22:14:53 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-
-(* legacy ML bindings *)
-
-val converse_rtranclE = thm "converse_rtranclE";
-val converse_rtranclE2 = thm "converse_rtranclE2";
-val converse_rtrancl_induct = thm "converse_rtrancl_induct";
-val converse_rtrancl_induct2 = thm "converse_rtrancl_induct2";
-val converse_rtrancl_into_rtrancl = thm "converse_rtrancl_into_rtrancl";
-val converse_trancl_induct = thm "converse_trancl_induct";
-val irrefl_tranclI = thm "irrefl_tranclI";
-val irrefl_trancl_rD = thm "irrefl_trancl_rD";
-val r_comp_rtrancl_eq = thm "r_comp_rtrancl_eq";
-val r_into_rtrancl = thm "r_into_rtrancl";
-val r_into_trancl = thm "r_into_trancl";
-val rtranclE = thm "rtranclE";
-val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
-val rtrancl_converse = thm "rtrancl_converse";
-val rtrancl_converseD = thm "rtrancl_converseD";
-val rtrancl_converseI = thm "rtrancl_converseI";
-val rtrancl_idemp = thm "rtrancl_idemp";
-val rtrancl_idemp_self_comp = thm "rtrancl_idemp_self_comp";
-val rtrancl_induct = thm "rtrancl_induct";
-val rtrancl_induct2 = thm "rtrancl_induct2";
-val rtrancl_into_rtrancl = thm "rtrancl_into_rtrancl";
-val rtrancl_into_trancl1 = thm "rtrancl_into_trancl1";
-val rtrancl_into_trancl2 = thm "rtrancl_into_trancl2";
-val rtrancl_mono = thm "rtrancl_mono";
-val rtrancl_r_diff_Id = thm "rtrancl_r_diff_Id";
-val rtrancl_refl = thm "rtrancl_refl";
-val rtrancl_reflcl = thm "rtrancl_reflcl";
-val rtrancl_subset = thm "rtrancl_subset";
-val rtrancl_subset_rtrancl = thm "rtrancl_subset_rtrancl";
-val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
-val rtrancl_trans = thm "rtrancl_trans";
-val tranclD = thm "tranclD";
-val tranclE = thm "tranclE";
-val trancl_converse = thm "trancl_converse";
-val trancl_converseD = thm "trancl_converseD";
-val trancl_converseI = thm "trancl_converseI";
-val trancl_induct = thm "trancl_induct";
-val trancl_insert = thm "trancl_insert";
-val trancl_into_rtrancl = thm "trancl_into_rtrancl";
-val trancl_into_trancl = thm "trancl_into_trancl";
-val trancl_into_trancl2 = thm "trancl_into_trancl2";
-val trancl_mono = thm "trancl_mono";
-val trancl_subset_Sigma = thm "trancl_subset_Sigma";
-val trancl_trans = thm "trancl_trans";
-val trancl_trans_induct = thm "trancl_trans_induct";
-val trans_rtrancl = thm "trans_rtrancl";
-val trans_trancl = thm "trans_trancl";
--- a/src/HOL/UNITY/Comp/Alloc.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Wed Dec 06 01:12:36 2006 +0100
@@ -288,6 +288,9 @@
bij_image_Collect_eq
ML {*
+local
+ val INT_D = thm "INT_D";
+in
(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
fun list_of_Int th =
(list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
@@ -295,6 +298,7 @@
handle THM _ => (list_of_Int (th RS INT_D))
handle THM _ => (list_of_Int (th RS bspec))
handle THM _ => [th];
+end;
*}
lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
--- a/src/HOL/UNITY/UNITY_tactics.ML Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Wed Dec 06 01:12:36 2006 +0100
@@ -7,6 +7,7 @@
*)
(*ListOrder*)
+val Domain_def = thm "Domain_def";
val Le_def = thm "Le_def";
val Ge_def = thm "Ge_def";
val prefix_def = thm "prefix_def";
--- a/src/HOL/W0/W0.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/W0/W0.thy Wed Dec 06 01:12:36 2006 +0100
@@ -353,7 +353,7 @@
apply (tactic {*
fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
thm "free_tv_subst_var" RS subsetD]
- addss (simpset() delsimps bex_simps
+ addss (simpset() delsimps (thms "bex_simps")
addsimps [thm "cod_def", thm "dom_def"])) 1 *})
done
@@ -581,7 +581,7 @@
apply (induct e)
txt {* case @{text "Var n"} *}
apply clarsimp
- apply (tactic {* fast_tac (HOL_cs addIs [nth_mem, subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
+ apply (tactic {* fast_tac (HOL_cs addIs [thm "nth_mem", subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
txt {* case @{text "Abs e"} *}
apply (simp add: free_tv_subst split add: split_bind)
apply (intro strip)
--- a/src/HOL/ex/MT.ML Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/ex/MT.ML Wed Dec 06 01:12:36 2006 +0100
@@ -86,7 +86,7 @@
by (assume_tac 1);
by (blast_tac (claset() addSIs [cih]) 1);
by (rtac (monoh RS monoD RS subsetD) 1);
-by (rtac Un_upper2 1);
+by (rtac (thm "Un_upper2") 1);
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
qed "gfp_coind2";
@@ -141,7 +141,7 @@
(* Monotonicity of eval_fun *)
-Goalw [mono_def, eval_fun_def] "mono(eval_fun)";
+Goalw [thm "mono_def", eval_fun_def] "mono(eval_fun)";
by infsys_mono_tac;
qed "eval_fun_mono";
@@ -259,7 +259,7 @@
(* Elaborations *)
(* ############################################################ *)
-Goalw [mono_def, elab_fun_def] "mono(elab_fun)";
+Goalw [thm "mono_def", elab_fun_def] "mono(elab_fun)";
by infsys_mono_tac;
qed "elab_fun_mono";
@@ -480,7 +480,7 @@
(* Monotonicity of hasty_fun *)
-Goalw [mono_def, hasty_fun_def] "mono(hasty_fun)";
+Goalw [thm "mono_def", hasty_fun_def] "mono(hasty_fun)";
by infsys_mono_tac;
by (Blast_tac 1);
qed "mono_hasty_fun";
@@ -607,7 +607,7 @@
Goal "[| ve hastyenv te; v hasty t |] ==> \
\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
by (rewtac hasty_env_def);
-by (asm_full_simp_tac (simpset() delsimps mem_simps
+by (asm_full_simp_tac (simpset() delsimps thms "mem_simps"
addsimps [ve_dom_owr, te_dom_owr]) 1);
by (safe_tac HOL_cs);
by (excluded_middle_tac "ev=x" 1);
@@ -651,12 +651,12 @@
by (etac elab_fn 1);
by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);
-by (asm_simp_tac (simpset() delsimps mem_simps addsimps [ve_dom_owr]) 1);
+by (asm_simp_tac (simpset() delsimps thms "mem_simps" addsimps [ve_dom_owr]) 1);
by (safe_tac HOL_cs);
by (excluded_middle_tac "ev2=ev1a" 1);
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (asm_simp_tac (simpset() delsimps mem_simps
+by (asm_simp_tac (simpset() delsimps thms "mem_simps"
addsimps [ve_app_owr1, te_app_owr1]) 1);
by (Blast_tac 1);
qed "consistency_fix";
--- a/src/HOL/ex/reflection.ML Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/ex/reflection.ML Wed Dec 06 01:12:36 2006 +0100
@@ -14,6 +14,9 @@
= struct
val ext2 = thm "ext2";
+val nth_Cons_0 = thm "nth_Cons_0";
+val nth_Cons_Suc = thm "nth_Cons_Suc";
+
(* Make a congruence rule out of a defining equation for the interpretation *)
(* th is one defining equation of f, i.e.
th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)