# HG changeset patch
# User wenzelm
# Date 1176672352 -7200
# Node ID f44439cdce776e2ac0f00dbf1dd4545a52098aaa
# Parent  9ab51bac6287ea795814f481e83aec103a7e554f
read prop as prop, not term;

diff -r 9ab51bac6287 -r f44439cdce77 src/HOL/Integ/IntDef.thy
--- 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
diff -r 9ab51bac6287 -r f44439cdce77 src/HOL/Real/PReal.thy
--- 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*}
diff -r 9ab51bac6287 -r f44439cdce77 src/Pure/Isar/constdefs.ML
--- 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;
diff -r 9ab51bac6287 -r f44439cdce77 src/ZF/Constructible/Datatype_absolute.thy
--- 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
diff -r 9ab51bac6287 -r f44439cdce77 src/ZF/Constructible/Relative.thy
--- 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)"
 
 
diff -r 9ab51bac6287 -r f44439cdce77 src/ZF/OrderArith.thy
--- 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")
diff -r 9ab51bac6287 -r f44439cdce77 src/ZF/WF.thy
--- 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"