# HG changeset patch # User wenzelm # Date 1165363956 -3600 # Node ID c68717c16013c99837c38802a9c91345786d771f # Parent 2d811ae6752a3c44beac1ac20e37784f4608fade removed legacy ML bindings; diff -r 2d811ae6752a -r c68717c16013 src/HOL/Bali/AxCompl.thy --- 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) diff -r 2d811ae6752a -r c68717c16013 src/HOL/Datatype.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/Datatype.thy --- 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 diff -r 2d811ae6752a -r c68717c16013 src/HOL/Finite_Set.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/HoareParallel/Gar_Coll.thy --- 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 *} diff -r 2d811ae6752a -r c68717c16013 src/HOL/HoareParallel/Mul_Gar_Coll.thy --- 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 *} diff -r 2d811ae6752a -r c68717c16013 src/HOL/IsaMakefile --- 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 \ diff -r 2d811ae6752a -r c68717c16013 src/HOL/Lambda/Commutation.thy --- 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) diff -r 2d811ae6752a -r c68717c16013 src/HOL/List.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/Nat.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/Nominal/nominal_atoms.ML --- 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 diff -r 2d811ae6752a -r c68717c16013 src/HOL/Nominal/nominal_package.ML --- 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, diff -r 2d811ae6752a -r c68717c16013 src/HOL/Nominal/nominal_permeq.ML --- 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 diff -r 2d811ae6752a -r c68717c16013 src/HOL/Orderings.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/Relation.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/Set.ML --- 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; diff -r 2d811ae6752a -r c68717c16013 src/HOL/Set.thy --- 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 diff -r 2d811ae6752a -r c68717c16013 src/HOL/Transitive_Closure.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/UNITY/Comp/Alloc.thy --- 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] diff -r 2d811ae6752a -r c68717c16013 src/HOL/UNITY/UNITY_tactics.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/W0/W0.thy --- 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) diff -r 2d811ae6752a -r c68717c16013 src/HOL/ex/MT.ML --- 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"; diff -r 2d811ae6752a -r c68717c16013 src/HOL/ex/reflection.ML --- 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)" *)