Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL/prob_extra.imp
changeset 44763 b50d5d694838
parent 39302 d7728f65b353 
--- a/src/HOL/Import/HOL/prob_extra.imp	Wed Sep 07 00:08:09 2011 +0200
+++ b/src/HOL/Import/HOL/prob_extra.imp	Wed Sep 07 07:59:45 2011 +0900
@@ -23,9 +23,9 @@
   "REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X"
   "REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE"
   "REAL_POW" > "RealDef.power_real_of_nat"
-  "REAL_LE_INV_LE" > "Rings.le_imp_inverse_le"
-  "REAL_LE_EQ" > "Set.basic_trans_rules_26"
-  "REAL_INVINV_ALL" > "Rings.inverse_inverse_eq"
+  "REAL_LE_INV_LE" > "Fields.linordered_field_class.le_imp_inverse_le"
+  "REAL_LE_EQ" > "Orderings.order_antisym"
+  "REAL_INVINV_ALL" > "Fields.division_ring_inverse_zero_class.inverse_inverse_eq"
   "REAL_INF_MIN" > "HOL4Prob.prob_extra.REAL_INF_MIN"
   "RAND_THM" > "HOL.arg_cong"
   "POW_HALF_TWICE" > "HOL4Prob.prob_extra.POW_HALF_TWICE"
@@ -59,7 +59,7 @@
   "INTER_UNION_COMPL" > "HOL4Base.pred_set.INTER_UNION_COMPL"
   "INTER_IS_EMPTY" > "HOL4Prob.prob_extra.INTER_IS_EMPTY"
   "INF_DEF_ALT" > "HOL4Prob.prob_extra.INF_DEF_ALT"
-  "HALF_POS" > "HOL4Prob.prob_extra.HALF_POS"
+  "HALF_POS" > "Series.half"
   "HALF_LT_1" > "HOL4Prob.prob_extra.HALF_LT_1"
   "HALF_CANCEL" > "HOL4Prob.prob_extra.HALF_CANCEL"
   "GSPEC_DEF_ALT" > "HOL4Prob.prob_extra.GSPEC_DEF_ALT"
@@ -73,7 +73,7 @@
   "EVEN_ODD_EXISTS_EQ" > "HOL4Prob.prob_extra.EVEN_ODD_EXISTS_EQ"
   "EVEN_ODD_BASIC" > "HOL4Prob.prob_extra.EVEN_ODD_BASIC"
   "EVEN_EXP_TWO" > "HOL4Prob.prob_extra.EVEN_EXP_TWO"
-  "EQ_EXT_EQ" > "Fun.fun_eq_iff"
+  "EQ_EXT_EQ" > "HOL.fun_eq_iff"
   "DIV_TWO_UNIQUE" > "HOL4Prob.prob_extra.DIV_TWO_UNIQUE"
   "DIV_TWO_MONO_EVEN" > "HOL4Prob.prob_extra.DIV_TWO_MONO_EVEN"
   "DIV_TWO_MONO" > "HOL4Prob.prob_extra.DIV_TWO_MONO"
isabelle