--- a/src/HOL/Import/HOL/HOL4Base.thy Thu Apr 29 06:01:48 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy Thu Apr 29 06:02:48 2004 +0200
@@ -2650,9 +2650,11 @@
lemma MEMBER_NOT_EMPTY: "ALL x. (EX xa. IN xa x) = (x ~= EMPTY)"
by (import pred_set MEMBER_NOT_EMPTY)
-constdefs
+consts
UNIV :: "'a => bool"
- "pred_set.UNIV == %x. True"
+
+defs
+ UNIV_def: "pred_set.UNIV == %x. True"
lemma UNIV_DEF: "pred_set.UNIV = (%x. True)"
by (import pred_set UNIV_DEF)
@@ -2719,9 +2721,11 @@
lemma PSUBSET_UNIV: "ALL x. PSUBSET x pred_set.UNIV = (EX xa. ~ IN xa x)"
by (import pred_set PSUBSET_UNIV)
-constdefs
+consts
UNION :: "('a => bool) => ('a => bool) => 'a => bool"
- "pred_set.UNION == %s t. GSPEC (%x. (x, IN x s | IN x t))"
+
+defs
+ UNION_def: "pred_set.UNION == %s t. GSPEC (%x. (x, IN x s | IN x t))"
lemma UNION_DEF: "ALL s t. pred_set.UNION s t = GSPEC (%x. (x, IN x s | IN x t))"
by (import pred_set UNION_DEF)
@@ -2761,9 +2765,11 @@
lemma EMPTY_UNION: "ALL x xa. (pred_set.UNION x xa = EMPTY) = (x = EMPTY & xa = EMPTY)"
by (import pred_set EMPTY_UNION)
-constdefs
+consts
INTER :: "('a => bool) => ('a => bool) => 'a => bool"
- "pred_set.INTER == %s t. GSPEC (%x. (x, IN x s & IN x t))"
+
+defs
+ INTER_def: "pred_set.INTER == %s t. GSPEC (%x. (x, IN x s & IN x t))"
lemma INTER_DEF: "ALL s t. pred_set.INTER s t = GSPEC (%x. (x, IN x s & IN x t))"
by (import pred_set INTER_DEF)
--- a/src/HOL/Import/ROOT.ML Thu Apr 29 06:01:48 2004 +0200
+++ b/src/HOL/Import/ROOT.ML Thu Apr 29 06:02:48 2004 +0200
@@ -3,30 +3,5 @@
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;
-
-
use_thy "HOL4Compat";
use_thy "HOL4Syntax";