--- a/src/HOL/Integ/IntDef.thy Sun Apr 15 23:25:50 2007 +0200
+++ b/src/HOL/Integ/IntDef.thy Sun Apr 15 23:25:52 2007 +0200
@@ -76,7 +76,7 @@
by (auto simp add: Integ_def intrel_def quotient_def)
text{*Reduces equality on abstractions to equality on representatives:
- @{term "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
+ @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
declare Abs_Integ_inject [simp] Abs_Integ_inverse [simp]
text{*Case analysis on the representation of an integer as an equivalence
--- a/src/HOL/Real/PReal.thy Sun Apr 15 23:25:50 2007 +0200
+++ b/src/HOL/Real/PReal.thy Sun Apr 15 23:25:52 2007 +0200
@@ -932,7 +932,7 @@
subsection{*Subtraction for Positive Reals*}
-text{*Gleason prop. 9-3.5(iv), page 123: proving @{term "A < B ==> \<exists>D. A + D =
+text{*Gleason prop. 9-3.5(iv), page 123: proving @{prop "A < B ==> \<exists>D. A + D =
B"}. We define the claimed @{term D} and show that it is a positive real*}
text{*Part 1 of Dedekind sections definition*}
--- a/src/Pure/Isar/constdefs.ML Sun Apr 15 23:25:50 2007 +0200
+++ b/src/Pure/Isar/constdefs.ML Sun Apr 15 23:25:52 2007 +0200
@@ -22,7 +22,7 @@
(** add_constdefs(_i) **)
-fun gen_constdef prep_vars prep_term prep_att
+fun gen_constdef prep_vars prep_prop prep_att
structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
let
fun err msg ts = error (cat_lines (msg :: map (Sign.string_of_term thy) ts));
@@ -36,7 +36,7 @@
struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
ProofContext.add_fixes_legacy [(x, T, mx)] #> snd #> pair (SOME x, mx)));
- val prop = prep_term var_ctxt raw_prop;
+ val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
val _ = (case d of NONE => () | SOME c' =>
if c <> c' then
@@ -53,15 +53,15 @@
|> PureThy.add_defs_i false [((name, def), atts)] |> snd;
in ((c, T), thy') end;
-fun gen_constdefs prep_vars prep_term prep_att (raw_structs, specs) thy =
+fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
let
val ctxt = ProofContext.init thy;
val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
- val (decls, thy') = fold_map (gen_constdef prep_vars prep_term prep_att structs) specs thy;
+ val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
- ProofContext.read_term_legacy Attrib.attribute;
-val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
+ ProofContext.read_prop_legacy Attrib.attribute;
+val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_prop (K I);
end;
--- a/src/ZF/Constructible/Datatype_absolute.thy Sun Apr 15 23:25:50 2007 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Sun Apr 15 23:25:52 2007 +0200
@@ -648,7 +648,7 @@
subsection {*Absoluteness for @{term transrec}*}
-text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
+text{* @{prop "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
definition
is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o" where
--- a/src/ZF/Constructible/Relative.thy Sun Apr 15 23:25:50 2007 +0200
+++ b/src/ZF/Constructible/Relative.thy Sun Apr 15 23:25:52 2007 +0200
@@ -1431,12 +1431,12 @@
definition
is_Nil :: "[i=>o, i] => o" where
- --{* because @{term "[] \<equiv> Inl(0)"}*}
+ --{* because @{prop "[] \<equiv> Inl(0)"}*}
"is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
definition
is_Cons :: "[i=>o,i,i,i] => o" where
- --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
+ --{* because @{prop "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
"is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
--- a/src/ZF/OrderArith.thy Sun Apr 15 23:25:50 2007 +0200
+++ b/src/ZF/OrderArith.thy Sun Apr 15 23:25:52 2007 +0200
@@ -369,7 +369,7 @@
done
text{*But note that the combination of @{text wf_imp_wf_on} and
- @{text wf_rvimage} gives @{term "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
+ @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
lemma wf_on_rvimage: "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
apply (rule wf_onI2)
apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba")
--- a/src/ZF/WF.thy Sun Apr 15 23:25:50 2007 +0200
+++ b/src/ZF/WF.thy Sun Apr 15 23:25:52 2007 +0200
@@ -84,7 +84,7 @@
text{*If @{term r} allows well-founded induction over @{term A}
then we have @{term "wf[A](r)"}. Premise is equivalent to
- @{term "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
+ @{prop "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
lemma wf_onI2:
assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A |]
==> y:B"