# HG changeset patch # User haftmann # Date 1164990148 -3600 # Node ID dea0914773f7ba6c03fa2b89fd8150d7a353a9c5 # Parent 1cbb1134cb6cd64ae920d8bdac3b81b27770b90f stripped some legacy bindings diff -r 1cbb1134cb6c -r dea0914773f7 src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Fri Dec 01 16:08:45 2006 +0100 +++ b/src/HOL/Auth/Public.thy Fri Dec 01 17:22:28 2006 +0100 @@ -402,15 +402,14 @@ insert_Key_singleton Key_not_used insert_Key_image Un_assoc [THEN sym] -ML -{* +ML {* val analz_image_freshK_lemma = thm "analz_image_freshK_lemma"; val analz_image_freshK_simps = thms "analz_image_freshK_simps"; +val imp_disjL = thm "imp_disjL"; -val analz_image_freshK_ss = - simpset() delsimps [image_insert, image_Un] - delsimps [imp_disjL] (*reduces blow-up*) - addsimps thms "analz_image_freshK_simps" +val analz_image_freshK_ss = simpset() delsimps [image_insert, image_Un] + delsimps [imp_disjL] (*reduces blow-up*) + addsimps thms "analz_image_freshK_simps" *} method_setup analz_freshK = {* diff -r 1cbb1134cb6c -r dea0914773f7 src/HOL/HOL.ML --- a/src/HOL/HOL.ML Fri Dec 01 16:08:45 2006 +0100 +++ b/src/HOL/HOL.ML Fri Dec 01 17:22:28 2006 +0100 @@ -20,7 +20,6 @@ val split_tac = Splitter.split_tac; val split_inside_tac = Splitter.split_inside_tac; -val split_asm_tac = Splitter.split_asm_tac; val op addsplits = Splitter.addsplits; val op delsplits = Splitter.delsplits; @@ -38,175 +37,100 @@ open BasicClassical; open Clasimp; -val eq_reflection = thm "eq_reflection"; -val def_imp_eq = thm "def_imp_eq"; -val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; -val ccontr = thm "ccontr"; -val impI = thm "impI"; -val impCE = thm "impCE"; -val notI = thm "notI"; -val notE = thm "notE"; -val iffI = thm "iffI"; -val iffCE = thm "iffCE"; -val conjI = thm "conjI"; -val conjE = thm "conjE"; -val disjCI = thm "disjCI"; -val disjE = thm "disjE"; -val TrueI = thm "TrueI"; -val FalseE = thm "FalseE"; -val allI = thm "allI"; +val all_conj_distrib = thm "all_conj_distrib"; +val all_dupE = thm "all_dupE" val allE = thm "allE"; -val exI = thm "exI"; -val exE = thm "exE"; -val ex_ex1I = thm "ex_ex1I"; -val the_equality = thm "the_equality"; -val mp = thm "mp"; -val rev_mp = thm "rev_mp" +val allI = thm "allI"; +val all_simps = thms "all_simps"; +val arg_cong = thm "arg_cong"; +val atomize_not = thm "atomize_not"; +val box_equals = thm "box_equals" +val case_split = thm "case_split_thm"; +val case_split_thm = thm "case_split_thm" +val cases_simp = thm "cases_simp"; +val ccontr = thm "ccontr"; +val choice_eq = thm "choice_eq" val classical = thm "classical"; -val subst = thm "subst"; -val refl = thm "refl"; -val sym = thm "sym"; -val trans = thm "trans"; -val arg_cong = thm "arg_cong"; -val iffD1 = thm "iffD1"; -val iffD2 = thm "iffD2"; -val disjE = thm "disjE"; +val cong = thm "cong" +val conj_comms = thms "conj_comms"; +val conj_cong = thm "conj_cong"; +val conjE = thm "conjE" val conjE = thm "conjE"; -val exE = thm "exE"; -val contrapos_nn = thm "contrapos_nn"; -val contrapos_pp = thm "contrapos_pp"; -val notnotD = thm "notnotD"; +val conjI = thm "conjI"; val conjunct1 = thm "conjunct1"; val conjunct2 = thm "conjunct2"; -val spec = thm "spec"; -val imp_cong = thm "imp_cong"; -val the_sym_eq_trivial = thm "the_sym_eq_trivial"; -val triv_forall_equality = thm "triv_forall_equality"; -val case_split = thm "case_split_thm"; -val ext = thm "ext" -val True_def = thm "True_def" -val All_def = thm "All_def" -val Ex_def = thm "Ex_def" -val False_def = thm "False_def" -val not_def = thm "not_def" -val and_def = thm "and_def" -val or_def = thm "or_def" -val Ex1_def = thm "Ex1_def" -val iff = thm "iff" -val True_or_False = thm "True_or_False" -val Let_def = thm "Let_def" -val if_def = thm "if_def" -val ssubst = thm "ssubst" -val box_equals = thm "box_equals" -val fun_cong = thm "fun_cong" -val cong = thm "cong" -val rev_iffD2 = thm "rev_iffD2" -val rev_iffD1 = thm "rev_iffD1" -val iffE = thm "iffE" -val eqTrueI = thm "eqTrueI" -val eqTrueE = thm "eqTrueE" -val all_dupE = thm "all_dupE" -val FalseE = thm "FalseE" -val False_neq_True = thm "False_neq_True" -val False_not_True = thm "False_not_True" -val True_not_False = thm "True_not_False" -val notI2 = thm "notI2" -val impE = thm "impE" -val not_sym = thm "not_sym" -val rev_contrapos = thm "rev_contrapos" -val conjE = thm "conjE" -val context_conjI = thm "context_conjI" -val disjI1 = thm "disjI1" -val disjI2 = thm "disjI2" -val rev_notE = thm "rev_notE" -val ex1I = thm "ex1I" -val ex1E = thm "ex1E" -val ex1_implies_ex = thm "ex1_implies_ex" -val the_equality = thm "the_equality" -val theI = thm "theI" -val theI' = thm "theI'" -val theI2 = thm "theI2" -val the1_equality = thm "the1_equality" -val excluded_middle = thm "excluded_middle" -val case_split_thm = thm "case_split_thm" -val exCI = thm "exCI" -val choice_eq = thm "choice_eq" -val eq_cong2 = thm "eq_cong2" -val if_cong = thm "if_cong" -val if_weak_cong = thm "if_weak_cong" -val let_weak_cong = thm "let_weak_cong" -val eq_cong2 = thm "eq_cong2" -val if_distrib = thm "if_distrib" -val restrict_to_left = thm "restrict_to_left" -val all_conj_distrib = thm "all_conj_distrib"; -val atomize_not = thm "atomize_not"; -val split_if = thm "split_if"; -val split_if_asm = thm "split_if_asm"; -val rev_conj_cong = thm "rev_conj_cong"; -val not_all = thm "not_all"; -val not_ex = thm "not_ex"; -val not_iff = thm "not_iff"; -val not_imp = thm "not_imp"; -val not_not = thm "not_not"; -val eta_contract_eq = thm "eta_contract_eq"; -val eq_ac = thms "eq_ac"; -val eq_commute = thm "eq_commute"; -val eq_sym_conv = thm "eq_commute"; -val neq_commute = thm "neq_commute"; -val conj_comms = thms "conj_comms"; -val conj_commute = thm "conj_commute"; -val conj_cong = thm "conj_cong"; -val conj_disj_distribL = thm "conj_disj_distribL"; -val conj_disj_distribR = thm "conj_disj_distribR"; -val conj_left_commute = thm "conj_left_commute"; -val disj_comms = thms "disj_comms"; -val disj_commute = thm "disj_commute"; -val disj_cong = thm "disj_cong"; -val disj_conj_distribL = thm "disj_conj_distribL"; -val disj_conj_distribR = thm "disj_conj_distribR"; -val disj_left_commute = thm "disj_left_commute"; -val eq_assoc = thm "eq_assoc"; -val eq_left_commute = thm "eq_left_commute"; -val ex_disj_distrib = thm "ex_disj_distrib"; -val if_P = thm "if_P"; -val if_bool_eq_disj = thm "if_bool_eq_disj"; -val if_def2 = thm "if_bool_eq_conj"; -val if_not_P = thm "if_not_P"; -val if_splits = thms "if_splits"; -val imp_all = thm "imp_all"; -val imp_conjL = thm "imp_conjL"; -val imp_conjR = thm "imp_conjR"; -val imp_disj_not1 = thm "imp_disj_not1"; -val imp_disj_not2 = thm "imp_disj_not2"; -val imp_ex = thm "imp_ex"; -val meta_eq_to_obj_eq = thm "def_imp_eq"; -val ex_simps = thms "ex_simps"; -val all_simps = thms "all_simps"; -val simp_thms = thms "simp_thms"; -val Eq_FalseI = thm "Eq_FalseI"; -val Eq_TrueI = thm "Eq_TrueI"; -val cases_simp = thm "cases_simp"; -val conj_assoc = thm "conj_assoc"; +val def_imp_eq = thm "def_imp_eq"; val de_Morgan_conj = thm "de_Morgan_conj"; val de_Morgan_disj = thm "de_Morgan_disj"; val disj_assoc = thm "disj_assoc"; -val disj_not1 = thm "disj_not1"; -val disj_not2 = thm "disj_not2"; -val if_False = thm "if_False"; -val if_True = thm "if_True"; -val if_bool_eq_conj = thm "if_bool_eq_conj"; +val disjCI = thm "disjCI"; +val disj_comms = thms "disj_comms"; +val disj_cong = thm "disj_cong"; +val disjE = thm "disjE"; +val disjI1 = thm "disjI1" +val disjI2 = thm "disjI2" +val eq_ac = thms "eq_ac"; +val eq_cong2 = thm "eq_cong2" +val Eq_FalseI = thm "Eq_FalseI"; +val eq_reflection = thm "eq_reflection"; +val Eq_TrueI = thm "Eq_TrueI"; +val Ex1_def = thm "Ex1_def" +val ex1E = thm "ex1E" +val ex1_implies_ex = thm "ex1_implies_ex" +val ex1I = thm "ex1I" +val excluded_middle = thm "excluded_middle" +val ex_disj_distrib = thm "ex_disj_distrib"; +val exE = thm "exE"; +val exI = thm "exI"; +val ex_simps = thms "ex_simps"; +val ext = thm "ext" +val FalseE = thm "FalseE" +val FalseE = thm "FalseE"; +val fun_cong = thm "fun_cong" val if_cancel = thm "if_cancel"; val if_eq_cancel = thm "if_eq_cancel"; +val if_False = thm "if_False"; val iff_conv_conj_imp = thm "iff_conv_conj_imp"; +val iffD1 = thm "iffD1"; +val iffD2 = thm "iffD2"; +val iffI = thm "iffI"; +val iff = thm "iff" +val if_splits = thms "if_splits"; +val if_True = thm "if_True"; +val if_weak_cong = thm "if_weak_cong" +val imp_all = thm "imp_all"; val imp_cong = thm "imp_cong"; +val imp_conjL = thm "imp_conjL"; +val imp_conjR = thm "imp_conjR"; val imp_conv_disj = thm "imp_conv_disj"; -val imp_disj1 = thm "imp_disj1"; -val imp_disj2 = thm "imp_disj2"; -val imp_disjL = thm "imp_disjL"; -val simp_impliesI = thm "simp_impliesI"; -val simp_implies_cong = thm "simp_implies_cong"; +val impE = thm "impE" +val impI = thm "impI"; +val Let_def = thm "Let_def" +val meta_eq_to_obj_eq = thm "def_imp_eq"; +val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; +val mp = thm "mp"; +val not_all = thm "not_all"; +val notE = thm "notE"; +val not_ex = thm "not_ex"; +val not_iff = thm "not_iff"; +val notI = thm "notI"; +val not_not = thm "not_not"; +val not_sym = thm "not_sym" +val refl = thm "refl"; +val rev_mp = thm "rev_mp" val simp_implies_def = thm "simp_implies_def"; +val simp_thms = thms "simp_thms"; +val spec = thm "spec"; +val split_if = thm "split_if"; +val ssubst = thm "ssubst" +val subst = thm "subst"; +val sym = thm "sym"; +val the1_equality = thm "the1_equality" +val theI = thm "theI" +val theI' = thm "theI'" +val trans = thm "trans"; val True_implies_equals = thm "True_implies_equals"; +val TrueI = thm "TrueI"; structure HOL = struct diff -r 1cbb1134cb6c -r dea0914773f7 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Fri Dec 01 16:08:45 2006 +0100 +++ b/src/HOL/Lattices.thy Fri Dec 01 17:22:28 2006 +0100 @@ -3,7 +3,7 @@ Author: Tobias Nipkow *) -header {* Lattices via Locales *} +header {* Abstract lattices *} theory Lattices imports Orderings @@ -187,29 +187,4 @@ lemmas min_ac = min_max.inf_assoc min_max.inf_commute mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute] -text {* ML legacy bindings *} - -ML {* -val Least_def = thm "Least_def"; -val Least_equality = thm "Least_equality"; -val min_def = thm "min_def"; -val min_of_mono = thm "min_of_mono"; -val max_def = thm "max_def"; -val max_of_mono = thm "max_of_mono"; -val min_leastL = thm "min_leastL"; -val max_leastL = thm "max_leastL"; -val min_leastR = thm "min_leastR"; -val max_leastR = thm "max_leastR"; -val le_max_iff_disj = thm "le_max_iff_disj"; -val le_maxI1 = thm "le_maxI1"; -val le_maxI2 = thm "le_maxI2"; -val less_max_iff_disj = thm "less_max_iff_disj"; -val max_less_iff_conj = thm "max_less_iff_conj"; -val min_less_iff_conj = thm "min_less_iff_conj"; -val min_le_iff_disj = thm "min_le_iff_disj"; -val min_less_iff_disj = thm "min_less_iff_disj"; -val split_min = thm "split_min"; -val split_max = thm "split_max"; -*} - end diff -r 1cbb1134cb6c -r dea0914773f7 src/HOL/Orderings.ML --- a/src/HOL/Orderings.ML Fri Dec 01 16:08:45 2006 +0100 +++ b/src/HOL/Orderings.ML Fri Dec 01 17:22:28 2006 +0100 @@ -1,21 +1,6 @@ (* legacy ML bindings *) -val order_eq_refl = thm "order_eq_refl"; val order_less_irrefl = thm "order_less_irrefl"; -val order_le_less = thm "order_le_less"; -val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq"; -val order_less_imp_le = thm "order_less_imp_le"; -val order_less_not_sym = thm "order_less_not_sym"; -val order_less_asym = thm "order_less_asym"; -val order_less_trans = thm "order_less_trans"; -val order_le_less_trans = thm "order_le_less_trans"; -val order_less_le_trans = thm "order_less_le_trans"; -val order_less_imp_not_less = thm "order_less_imp_not_less"; -val order_less_imp_triv = thm "order_less_imp_triv"; -val order_less_imp_not_eq = thm "order_less_imp_not_eq"; -val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2"; -val linorder_less_linear = thm "linorder_less_linear"; -val linorder_cases = thm "linorder_cases"; val linorder_not_less = thm "linorder_not_less"; val linorder_not_le = thm "linorder_not_le"; val linorder_neq_iff = thm "linorder_neq_iff"; @@ -23,8 +8,10 @@ val order_refl = thm "order_refl"; val order_trans = thm "order_trans"; val order_antisym = thm "order_antisym"; -val order_less_le = thm "order_less_le"; -val linorder_linear = thm "linorder_linear"; 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 1cbb1134cb6c -r dea0914773f7 src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Dec 01 16:08:45 2006 +0100 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Dec 01 17:22:28 2006 +0100 @@ -104,6 +104,7 @@ text{*This ML code does the inductions directly.*} ML{* val ns_constrainsI = thm "ns_constrainsI"; +val impCE = thm "impCE"; fun ns_constrains_tac(cs,ss) i = SELECT_GOAL diff -r 1cbb1134cb6c -r dea0914773f7 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Fri Dec 01 16:08:45 2006 +0100 +++ b/src/HOLCF/domain/theorems.ML Fri Dec 01 17:22:28 2006 +0100 @@ -213,6 +213,7 @@ val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args)); in Library.foldr mk_ex (vns, conj) end; + val conj_assoc = thm "conj_assoc"; val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons); val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start; val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1; @@ -350,6 +351,7 @@ end; local + val rev_contrapos = thm "rev_contrapos"; fun con_strict (con, args) = let fun one_strict vn = @@ -457,6 +459,7 @@ end; val sel_rews = sel_stricts @ sel_defins @ sel_apps; +val rev_contrapos = thm "rev_contrapos"; val distincts_le = let