--- a/src/HOL/Univ.ML Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Univ.ML Mon Mar 04 14:37:33 1996 +0100
@@ -8,47 +8,6 @@
open Univ;
-(** LEAST -- the least number operator **)
-
-
-val [prem1,prem2] = goalw Univ.thy [Least_def]
- "[| P(k); !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
-by (rtac select_equality 1);
-by (fast_tac (HOL_cs addSIs [prem1,prem2]) 1);
-by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addSIs [prem1] addSDs [prem2]) 1);
-qed "Least_equality";
-
-val [prem] = goal Univ.thy "P(k) ==> P(LEAST x.P(x))";
-by (rtac (prem RS rev_mp) 1);
-by (res_inst_tac [("n","k")] less_induct 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
-by (assume_tac 1);
-by (assume_tac 2);
-by (fast_tac HOL_cs 1);
-qed "LeastI";
-
-(*Proof is almost identical to the one above!*)
-val [prem] = goal Univ.thy "P(k) ==> (LEAST x.P(x)) <= k";
-by (rtac (prem RS rev_mp) 1);
-by (res_inst_tac [("n","k")] less_induct 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
-by (assume_tac 1);
-by (rtac le_refl 2);
-by (fast_tac (HOL_cs addIs [less_imp_le,le_trans]) 1);
-qed "Least_le";
-
-val [prem] = goal Univ.thy "k < (LEAST x.P(x)) ==> ~P(k)";
-by (rtac notI 1);
-by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
-by (rtac prem 1);
-qed "not_less_Least";
-
-
(** apfst -- can be used in similar type definitions **)
goalw Univ.thy [apfst_def] "apfst f (a,b) = (f(a),b)";