1) all theorems in Orderings can now be given as a parameter
2) new function Theory.defs_of
3) new functions Defs.overloading_info and Defs.is_overloaded

--- a/src/HOL/Orderings.thy	Thu Jul 07 18:38:00 2005 +0200
+++ b/src/HOL/Orderings.thy	Thu Jul 07 19:01:04 2005 +0200
@@ -346,6 +346,7 @@
     val neq_le_trans = thm "order_neq_le_trans";
     val less_imp_neq = thm "less_imp_neq";
     val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
+    val not_sym = thm "not_sym";
     val decomp_part = decomp_gen ["Orderings.order"];
     val decomp_lin = decomp_gen ["Orderings.linorder"];
 

--- a/src/Provers/order.ML	Thu Jul 07 18:38:00 2005 +0200
+++ b/src/Provers/order.ML	Thu Jul 07 19:01:04 2005 +0200
@@ -44,6 +44,7 @@
   val le_trans: thm  (* [| x <= y; y <= z |] ==> x <= z *)
   val le_neq_trans : thm (* [| x <= y ; x ~= y |] ==> x < y *)
   val neq_le_trans : thm (* [| x ~= y ; x <= y |] ==> x < y *)
+  val not_sym : thm (* x ~= y ==> y ~= x *)
 
   (* Additional theorems for linear orders *)
   val not_lessD: thm (* ~(x < y) ==> y <= x *)
@@ -137,7 +138,7 @@
     | "~="  => if (x aconv y) then 
                   raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
                else [ NotEq (x, y, Asm n),
-                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
+                      NotEq (y, x,Thm ( [Asm n], Less.not_sym))] 
     | _     => error ("partial_tac: unknown relation symbol ``" ^ rel ^
                  "''returned by decomp_part."))
   | NONE => [];
@@ -167,7 +168,7 @@
     | "~="  => if (x aconv y) then 
                   raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
                else [ NotEq (x, y, Asm n),
-                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] 
+                      NotEq (y, x,Thm ( [Asm n], Less.not_sym))] 
     | _     => error ("linear_tac: unknown relation symbol ``" ^ rel ^
                  "''returned by decomp_lin."))
   | NONE => [];
@@ -785,10 +786,10 @@
      (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
        ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
           if  (x aconv x' andalso y aconv y') then p 
-	  else Thm ([p], thm "not_sym")
+	  else Thm ([p], Less.not_sym)
      | ( SOME (Less (x, y, p)), NotEq (x', y', _)) => 
           if x aconv x' andalso y aconv y' then (Thm ([p], Less.less_imp_neq))
-          else (Thm ([(Thm ([p], Less.less_imp_neq))], thm "not_sym"))
+          else (Thm ([(Thm ([p], Less.less_imp_neq))], Less.not_sym))
      | _ => raise Cannot) 
    ) else (
    
@@ -810,11 +811,11 @@
 	    	if e subsumes subgoal then (
 		     case e of (Less (u, v, q)) => (
 		       if u aconv x andalso v aconv y then (Thm ([q], Less.less_imp_neq))
-		       else (Thm ([(Thm ([q], Less.less_imp_neq))], thm "not_sym"))
+		       else (Thm ([(Thm ([q], Less.less_imp_neq))], Less.not_sym))
 		     )
 		     |    (NotEq (u,v, q)) => (
 		       if u aconv x andalso v aconv y then q
-		       else (Thm ([q],  thm "not_sym"))
+		       else (Thm ([q],  Less.not_sym))
 		     )
 		 )
                 (* if SCC_x is linked to SCC_y via edge e *)
@@ -843,7 +844,7 @@
 		     case e of (Less (_, _,_)) => (
 		        let val xypath = (completeTermPath y u (List.nth(sccSubgraphs, ui)) ) @ [e] @ (completeTermPath v x (List.nth(sccSubgraphs, vi)) )
 			    val xyLesss = transPath (tl xypath, hd xypath)
-			in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , thm "not_sym")) end ) 
+			in (Thm ([(Thm ([getprf xyLesss], Less.less_imp_neq))] , Less.not_sym)) end ) 
 		     | _ => (
 		        
 			let val yupath = completeTermPath y u (List.nth(sccSubgraphs, ui))
@@ -857,7 +858,7 @@
 			    val y_eq_u =  (Thm ([(getprf yuLesss),(getprf uyLesss)], Less.eqI))
 			    val v_eq_x =  (Thm ([(getprf vxLesss),(getprf xvLesss)], Less.eqI))
 			in
-			    (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], thm "not_sym"))
+			    (Thm ([(Thm ([y_eq_u , (getprf e), v_eq_x ], Less.eq_neq_eq_imp_neq))], Less.not_sym))
 		        end
 		       )
 		  ) else (
@@ -871,7 +872,7 @@
 	                        val xr = dfs_int_reachable sccGraph_transpose xi
 		               in 
 		                case  (findLess e y x yi xi yr xr) of 
-		                      (SOME prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], thm "not_sym")) 
+		                      (SOME prf) => (Thm ([(Thm ([prf], Less.less_imp_neq))], Less.not_sym)) 
                                       | _ => processNeqEdges es
 		               end)
 		 ) end) 

--- a/src/Pure/defs.ML	Thu Jul 07 18:38:00 2005 +0200
+++ b/src/Pure/defs.ML	Thu Jul 07 19:01:04 2005 +0200
@@ -35,6 +35,10 @@
   val set_chain_history : bool -> unit
   val chain_history : unit -> bool
 
+  datatype overloadingstate = Open | Closed | Final
+  val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option
+  val is_overloaded : graph -> string -> bool
+
 end
 
 structure Defs :> DEFS = struct
@@ -42,7 +46,7 @@
 type tyenv = Type.tyenv
 type edgelabel = (int * typ * typ * (typ * string * string) list)
 
-datatype forwardstate = Open | Closed | Final
+datatype overloadingstate = Open | Closed | Final
 
 datatype node = Node of
          typ  (* most general type of constant *)
@@ -53,7 +57,7 @@
              (* a table of all back referencing defnodes to this node, 
                 indexed by node name of the defnodes *)
          * typ list (* a list of all finalized types *)
-         * forwardstate
+         * overloadingstate
      
      and defnode = Defnode of
          typ  (* type of the constant in this particular definition *)
@@ -653,6 +657,21 @@
           Symtab.update_new ((name, ftys), finals)) 
       (Symtab.empty, graph)
 
+fun overloading_info (_, axmap, _, graph) c = 
+    let
+      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
+    in
+      case Symtab.lookup (graph, c) of
+        NONE => NONE
+      | SOME (Node (ty, defnodes, _, _, state)) =>
+        SOME (ty, map translate (Symtab.dest defnodes), state)
+    end
+      
+fun is_overloaded g c = 
+    case overloading_info g c of
+      NONE => false
+    | SOME (_, l, _) => length l >= 2
+
 end;
 		
 (*

--- a/src/Pure/theory.ML	Thu Jul 07 18:38:00 2005 +0200
+++ b/src/Pure/theory.ML	Thu Jul 07 19:01:04 2005 +0200
@@ -38,6 +38,7 @@
   val oracle_space: theory -> NameSpace.T
   val axioms_of: theory -> (string * term) list
   val all_axioms_of: theory -> (string * term) list
+  val defs_of : theory -> Defs.graph
   val self_ref: theory -> theory_ref
   val deref: theory_ref -> theory
   val merge: theory * theory -> theory                     (*exception TERM*)
@@ -178,6 +179,8 @@
 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
 fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
 
+fun defs_of thy = (case rep_theory thy of {defs=D, ...} => D)
+
 fun requires thy name what =
   if Context.exists_name name thy then ()
   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);