# HG changeset patch
# User wenzelm
# Date 1083442036 -7200
# Node ID 49873d345a3962fb36dab34e6150cac45054c712
# Parent  4deda204e1d8f94e9fefe733acc850e9d4e6a9fd
removed 'constdefs' hack;

diff -r 4deda204e1d8 -r 49873d345a39 src/HOL/Import/HOL/HOL4Real.thy
--- a/src/HOL/Import/HOL/HOL4Real.thy	Sat May 01 22:05:05 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Sat May 01 22:07:16 2004 +0200
@@ -584,9 +584,11 @@
 (ALL n m f. sumc n (Suc m) f = sumc n m f + f (n + m))"
   by (import real sumc)
 
-constdefs
+consts
   sum :: "nat * nat => (nat => real) => real" 
-  "real.sum == split sumc"
+
+defs
+  sum_def: "real.sum == split sumc"
 
 lemma SUM_DEF: "ALL m n f. real.sum (m, n) f = sumc m n f"
   by (import real SUM_DEF)
@@ -1170,9 +1172,11 @@
 
 ;setup_theory seq
 
-constdefs
+consts
   "-->" :: "(nat => real) => real => bool" ("-->")
-  "--> == %x x0. tends x x0 (mtop mr1, nat_ge)"
+
+defs
+  "-->_def": "--> == %x x0. tends x x0 (mtop mr1, nat_ge)"
 
 lemma tends_num_real: "ALL x x0. --> x x0 = tends x x0 (mtop mr1, nat_ge)"
   by (import seq tends_num_real)
@@ -1396,9 +1400,11 @@
 lemma SUBSEQ_SUC: "ALL f. subseq f = (ALL n. f n < f (Suc n))"
   by (import seq SUBSEQ_SUC)
 
-constdefs
+consts
   mono :: "(nat => real) => bool" 
-  "(op ==::((nat => real) => bool) => ((nat => real) => bool) => prop)
+
+defs
+  mono_def: "(op ==::((nat => real) => bool) => ((nat => real) => bool) => prop)
  (seq.mono::(nat => real) => bool)
  (%f::nat => real.
      (op |::bool => bool => bool)
diff -r 4deda204e1d8 -r 49873d345a39 src/HOL/Import/HOL/ROOT.ML
--- a/src/HOL/Import/HOL/ROOT.ML	Sat May 01 22:05:05 2004 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Sat May 01 22:07:16 2004 +0200
@@ -3,29 +3,6 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-(* FIXME tmp hack to get generated theories work *)
-
-local
-
-fun old_add_constdefs args thy =
-  thy
-  |> Theory.add_consts (map fst args)
-  |> IsarThy.add_defs (false, map (fn ((c, _, mx), s) =>
-    ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
-
-structure P = OuterParse and K = OuterSyntax.Keyword;
-
-val constdefsP =
-  OuterSyntax.command "constdefs" "declare and define constants (old style)"
-    K.thy_decl
-    (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o old_add_constdefs));
-
-in
-
-val _ = OuterSyntax.add_parsers [constdefsP];
-
-end;
-
 with_path ".." use_thy "HOL4Compat";
 with_path ".." use_thy "HOL4Syntax";
 setmp quick_and_dirty true use_thy "HOL4Prob";