--- a/src/HOL/Import/proof_kernel.ML Fri Jun 11 16:52:17 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Jun 11 17:14:01 2010 +0200
@@ -1946,7 +1946,7 @@
val p3 = string_of_mixfix csyn
val p4 = smart_string_of_cterm crhs
in
- add_dump ("constdefs\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ "\n " ^ p4) thy''
+ add_dump ("definition\n " ^ p1 ^ " :: \"" ^ p2 ^ "\" "^ p3 ^ " where\n " ^ p4) thy''
end
else
add_dump ("consts\n " ^ quotename constname ^ " :: \"" ^
@@ -2139,18 +2139,6 @@
end
handle e => (message "exception in new_type_definition"; print_exn e)
-fun add_dump_constdefs thy defname constname rhs ty =
- let
- val n = quotename constname
- val t = Syntax.string_of_typ_global thy ty
- val syn = string_of_mixfix (mk_syn thy constname)
- (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
- val eq = quote (constname ^ " == "^rhs)
- val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
- in
- add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy
- end
-
fun add_dump_syntax thy name =
let
val n = quotename name
--- a/src/HOL/Tools/refute.ML Fri Jun 11 16:52:17 2010 +0200
+++ b/src/HOL/Tools/refute.ML Fri Jun 11 17:14:01 2010 +0200
@@ -517,7 +517,7 @@
end
(* ------------------------------------------------------------------------- *)
-(* get_def: looks up the definition of a constant, as created by "constdefs" *)
+(* get_def: looks up the definition of a constant *)
(* ------------------------------------------------------------------------- *)
(* theory -> string * Term.typ -> (string * Term.term) option *)
@@ -711,7 +711,7 @@
(* Note: currently we use "inverse" functions to the definitional *)
(* mechanisms provided by Isabelle/HOL, e.g. for "axclass", *)
- (* "typedef", "constdefs". A more general approach could consider *)
+ (* "typedef", "definition". A more general approach could consider *)
(* *every* axiom of the theory and collect it if it has a constant/ *)
(* type/typeclass in common with the term 't'. *)
--- a/src/ZF/ZF.thy Fri Jun 11 16:52:17 2010 +0200
+++ b/src/ZF/ZF.thy Fri Jun 11 17:14:01 2010 +0200
@@ -199,10 +199,7 @@
finalconsts
0 Pow Inf Union PrimReplace mem
-defs
-(*don't try to use constdefs: the declaration order is tightly constrained*)
-
- (* Bounded Quantifiers *)
+defs (* Bounded Quantifiers *)
Ball_def: "Ball(A, P) == \<forall>x. x\<in>A --> P(x)"
Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)"