# 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			\