Merge pull request #574 from binghe/rich_topology

hol-light's topology theory and dependents (up to 2015)

src/1/wlogLib.sml

@@ -74,7 +74,10 @@ none then "p_hyp" is just "hyp" else it is the splice of "p" with "hyp". The
 tuple returned is the aforementioned theorem and "P_hyp". *)
 fun wlog_rule vars p hyp t =
   let
-    val the = liteLib.the
+    (* val the = liteLib.the (broken in mosml) *)
+    fun the (SOME x) = x
+      | the _ = failwith "the: can't take \"the\" of NONE"
+
     fun forall vars t = list_mk_forall (vars, t)
     fun implies t1 t2 = mk_imp (t1, t2)
     val new_sg_t = forall vars (implies (case hyp of

src/finite_map/flookupLib.sml

@@ -3,6 +3,8 @@ struct
 
 open HolKernel boolLib bossLib finite_mapSyntax
 
+val ERR = mk_HOL_ERR "flookupLib"
+
 (* ------------------------------------------------------------------------- *)
 
 fun memoize size cmp f =

src/patricia/patricia_castsSyntax.sml

@@ -9,6 +9,8 @@ struct
 open Abbrev HolKernel pred_setSyntax wordsSyntax patriciaSyntax
      patricia_castsTheory;
 
+val ERR = mk_HOL_ERR "patricia_castsSyntax"
+
 (* ------------------------------------------------------------------------- *)
 
 fun mk_word_ptree_type (aty, bty) =

src/pred_set/src/pred_setScript.sml

@@ -1363,6 +1363,11 @@ val REST_DEF =
     new_definition
     ("REST_DEF", (“REST (s:'a set) = s DELETE (CHOICE s)”));
 
+val IN_REST = store_thm
+  ("IN_REST",
+  ``!x:'a. !s. x IN (REST s) <=> x IN s /\ ~(x = CHOICE s)``,
+    REWRITE_TAC [REST_DEF, IN_DELETE]);
+
 val CHOICE_NOT_IN_REST =
     store_thm
     ("CHOICE_NOT_IN_REST",