--- a/src/Pure/more_thm.ML Sat Mar 07 21:57:36 2009 +0100
+++ b/src/Pure/more_thm.ML Sat Mar 07 22:04:59 2009 +0100
@@ -55,6 +55,8 @@
val position_of: thm -> Position.T
val default_position: Position.T -> thm -> thm
val default_position_of: thm -> thm -> thm
+ val def_name: string -> string
+ val def_name_optional: string -> string -> string
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
val put_name_hint: string -> thm -> thm
@@ -278,6 +280,8 @@
(** specification primitives **)
+(* rules *)
+
fun add_axiom (b, prop) thy =
let
val b' = if Binding.is_empty b
@@ -342,6 +346,14 @@
val default_position_of = default_position o position_of;
+(* def_name *)
+
+fun def_name c = c ^ "_def";
+
+fun def_name_optional c "" = def_name c
+ | def_name_optional _ name = name;
+
+
(* unofficial theorem names *)
fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);