# HG changeset patch # User haftmann # Date 1178480964 -7200 # Node ID ede26eb5e549d0515e18a1e51cd002c644bcb5b6 # Parent 466599ecf610e96cb6c4de4db066528f6d8bac82 dropped HOL.ML diff -r 466599ecf610 -r ede26eb5e549 src/HOL/HOL.ML --- a/src/HOL/HOL.ML Sun May 06 21:49:23 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -(* - ID: $Id$ -*) - -(** legacy ML bindings **) - -val all_conj_distrib = thm "all_conj_distrib"; -val all_simps = thms "all_simps"; -val atomize_not = thm "atomize_not"; -val case_split = thm "case_split_thm"; -val case_split_thm = thm "case_split_thm" -val cases_simp = thm "cases_simp"; -val choice_eq = thm "choice_eq" -val cong = thm "cong" -val conj_comms = thms "conj_comms"; -val conj_cong = thm "conj_cong"; -val de_Morgan_conj = thm "de_Morgan_conj"; -val de_Morgan_disj = thm "de_Morgan_disj"; -val disj_assoc = thm "disj_assoc"; -val disj_comms = thms "disj_comms"; -val disj_cong = thm "disj_cong"; -val eq_ac = thms "eq_ac"; -val eq_cong2 = thm "eq_cong2" -val Eq_FalseI = thm "Eq_FalseI"; -val Eq_TrueI = thm "Eq_TrueI"; -val Ex1_def = thm "Ex1_def" -val ex_disj_distrib = thm "ex_disj_distrib"; -val ex_simps = thms "ex_simps"; -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 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 simp_implies_def = thm "simp_implies_def"; -val simp_thms = thms "simp_thms"; -val split_if = thm "split_if"; -val the1_equality = thm "the1_equality" -val theI = thm "theI" -val theI' = thm "theI'" -val True_implies_equals = thm "True_implies_equals"; diff -r 466599ecf610 -r ede26eb5e549 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun May 06 21:49:23 2007 +0200 +++ b/src/HOL/HOL.thy Sun May 06 21:49:24 2007 +0200 @@ -40,10 +40,10 @@ Ex1 :: "('a => bool) => bool" (binder "EX! " 10) Let :: "['a, 'a => 'b] => 'b" - "=" :: "['a, 'a] => bool" (infixl 50) - & :: "[bool, bool] => bool" (infixr 35) - "|" :: "[bool, bool] => bool" (infixr 30) - --> :: "[bool, bool] => bool" (infixr 25) + "op =" :: "['a, 'a] => bool" (infixl "=" 50) + "op &" :: "[bool, bool] => bool" (infixr "&" 35) + "op |" :: "[bool, bool] => bool" (infixr "|" 30) + "op -->" :: "[bool, bool] => bool" (infixr "-->" 25) local @@ -1463,7 +1463,7 @@ *} -subsection {* Legacy tactics *} +subsection {* Legacy tactics and ML bindings *} ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i); @@ -1478,6 +1478,49 @@ fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]); fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]; end; + +val all_conj_distrib = thm "all_conj_distrib"; +val all_simps = thms "all_simps"; +val atomize_not = thm "atomize_not"; +val case_split = thm "case_split_thm"; +val case_split_thm = thm "case_split_thm" +val cases_simp = thm "cases_simp"; +val choice_eq = thm "choice_eq" +val cong = thm "cong" +val conj_comms = thms "conj_comms"; +val conj_cong = thm "conj_cong"; +val de_Morgan_conj = thm "de_Morgan_conj"; +val de_Morgan_disj = thm "de_Morgan_disj"; +val disj_assoc = thm "disj_assoc"; +val disj_comms = thms "disj_comms"; +val disj_cong = thm "disj_cong"; +val eq_ac = thms "eq_ac"; +val eq_cong2 = thm "eq_cong2" +val Eq_FalseI = thm "Eq_FalseI"; +val Eq_TrueI = thm "Eq_TrueI"; +val Ex1_def = thm "Ex1_def" +val ex_disj_distrib = thm "ex_disj_distrib"; +val ex_simps = thms "ex_simps"; +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 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 simp_implies_def = thm "simp_implies_def"; +val simp_thms = thms "simp_thms"; +val split_if = thm "split_if"; +val the1_equality = thm "the1_equality" +val theI = thm "theI" +val theI' = thm "theI'" +val True_implies_equals = thm "True_implies_equals"; *} end diff -r 466599ecf610 -r ede26eb5e549 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun May 06 21:49:23 2007 +0200 +++ b/src/HOL/IsaMakefile Sun May 06 21:49:24 2007 +0200 @@ -85,7 +85,7 @@ $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML \ $(SRC)/TFL/utils.ML ATP_Linkup.thy Accessible_Part.thy \ Code_Generator.thy Datatype.thy Divides.thy Equiv_Relations.thy \ - Extraction.thy Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.ML \ + Extraction.thy Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy \ 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 Integ/Presburger.thy \