--- 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