# HG changeset patch
# User wenzelm
# Date 781975926 -3600
# Node ID 7f25cc9067e7539a5ac0cee03a179e0d65988375
# Parent  b344bf6241432f6453dd6cf2f28314ad8ed16711
prove_subclass, prove_arity now exported;
minor internal changes;

diff -r b344bf624143 -r 7f25cc9067e7 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Oct 12 16:31:01 1994 +0100
+++ b/src/Pure/axclass.ML	Wed Oct 12 16:32:06 1994 +0100
@@ -21,6 +21,10 @@
     val add_inst_arity: string * sort list * class list -> string list
       -> thm list -> tactic option -> theory -> theory
     val axclass_tac: theory -> thm list -> tactic
+    val prove_subclass: theory -> class * class -> thm list
+      -> tactic option -> thm
+    val prove_arity: theory -> string * sort list * class -> thm list
+      -> tactic option -> thm
     val goal_subclass: theory -> class * class -> thm list
     val goal_arity: theory -> string * sort list * class -> thm list
   end
@@ -60,14 +64,6 @@
 val get_axioms = mapfilter o get_ax;
 
 
-(* is_defn *)
-
-fun is_defn thm =
-  (case #prop (rep_thm thm) of
-    Const ("==", _) $ _ $ _ => true
-  | _ => false);
-
-
 
 (** abstract syntax operations **)
 
@@ -249,10 +245,12 @@
   (2) rewrite goals using user supplied definitions
   (3) repeatedly resolve goals with user supplied non-definitions*)
 
+val is_def = is_equals o #prop o rep_thm;
+
 fun axclass_tac thy thms =
   TRY (REPEAT_FIRST (resolve_tac (class_axms thy))) THEN
-  TRY (rewrite_goals_tac (filter is_defn thms)) THEN
-  TRY (REPEAT_FIRST (resolve_tac (filter_out is_defn thms)));
+  TRY (rewrite_goals_tac (filter is_def thms)) THEN
+  TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms)));
 
 
 (* provers *)
@@ -268,7 +266,7 @@
   handle ERROR => error ("The error(s) above occurred while trying to prove "
     ^ quote (str_of sig_prop));
 
-val prove_classrel =
+val prove_subclass =
   prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2);
 
 val prove_arity =
@@ -289,7 +287,7 @@
 
 fun add_inst_subclass (c1, c2) axms thms usr_tac thy =
   add_classrel_thms
-  [prove_classrel thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy;
+  [prove_subclass thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy;
 
 fun add_inst_arity (t, ss, cs) axms thms usr_tac thy =
   let