read prop as prop, not term;
authorwenzelm
Sun Apr 15 23:25:52 2007 +0200 (2007-04-15)
changeset 22710f44439cdce77
parent 22709 9ab51bac6287
child 22711 0b18739c3e81
read prop as prop, not term;
src/HOL/Integ/IntDef.thy
src/HOL/Real/PReal.thy
src/Pure/Isar/constdefs.ML
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Relative.thy
src/ZF/OrderArith.thy
src/ZF/WF.thy
     1.1 --- a/src/HOL/Integ/IntDef.thy	Sun Apr 15 23:25:50 2007 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Sun Apr 15 23:25:52 2007 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  by (auto simp add: Integ_def intrel_def quotient_def)
     1.5  
     1.6  text{*Reduces equality on abstractions to equality on representatives:
     1.7 -  @{term "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
     1.8 +  @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
     1.9  declare Abs_Integ_inject [simp]  Abs_Integ_inverse [simp]
    1.10  
    1.11  text{*Case analysis on the representation of an integer as an equivalence
     2.1 --- a/src/HOL/Real/PReal.thy	Sun Apr 15 23:25:50 2007 +0200
     2.2 +++ b/src/HOL/Real/PReal.thy	Sun Apr 15 23:25:52 2007 +0200
     2.3 @@ -932,7 +932,7 @@
     2.4  
     2.5  subsection{*Subtraction for Positive Reals*}
     2.6  
     2.7 -text{*Gleason prop. 9-3.5(iv), page 123: proving @{term "A < B ==> \<exists>D. A + D =
     2.8 +text{*Gleason prop. 9-3.5(iv), page 123: proving @{prop "A < B ==> \<exists>D. A + D =
     2.9  B"}. We define the claimed @{term D} and show that it is a positive real*}
    2.10  
    2.11  text{*Part 1 of Dedekind sections definition*}
     3.1 --- a/src/Pure/Isar/constdefs.ML	Sun Apr 15 23:25:50 2007 +0200
     3.2 +++ b/src/Pure/Isar/constdefs.ML	Sun Apr 15 23:25:52 2007 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4  
     3.5  (** add_constdefs(_i) **)
     3.6  
     3.7 -fun gen_constdef prep_vars prep_term prep_att
     3.8 +fun gen_constdef prep_vars prep_prop prep_att
     3.9      structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
    3.10    let
    3.11      fun err msg ts = error (cat_lines (msg :: map (Sign.string_of_term thy) ts));
    3.12 @@ -36,7 +36,7 @@
    3.13            struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
    3.14              ProofContext.add_fixes_legacy [(x, T, mx)] #> snd #> pair (SOME x, mx)));
    3.15  
    3.16 -    val prop = prep_term var_ctxt raw_prop;
    3.17 +    val prop = prep_prop var_ctxt raw_prop;
    3.18      val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
    3.19      val _ = (case d of NONE => () | SOME c' =>
    3.20        if c <> c' then
    3.21 @@ -53,15 +53,15 @@
    3.22        |> PureThy.add_defs_i false [((name, def), atts)] |> snd;
    3.23    in ((c, T), thy') end;
    3.24  
    3.25 -fun gen_constdefs prep_vars prep_term prep_att (raw_structs, specs) thy =
    3.26 +fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
    3.27    let
    3.28      val ctxt = ProofContext.init thy;
    3.29      val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
    3.30 -    val (decls, thy') = fold_map (gen_constdef prep_vars prep_term prep_att structs) specs thy;
    3.31 +    val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
    3.32    in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
    3.33  
    3.34  val add_constdefs = gen_constdefs ProofContext.read_vars_legacy
    3.35 -  ProofContext.read_term_legacy Attrib.attribute;
    3.36 -val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I);
    3.37 +  ProofContext.read_prop_legacy Attrib.attribute;
    3.38 +val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_prop (K I);
    3.39  
    3.40  end;
     4.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Sun Apr 15 23:25:50 2007 +0200
     4.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Sun Apr 15 23:25:52 2007 +0200
     4.3 @@ -648,7 +648,7 @@
     4.4  
     4.5  subsection {*Absoluteness for @{term transrec}*}
     4.6  
     4.7 -text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
     4.8 +text{* @{prop "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
     4.9  
    4.10  definition
    4.11    is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o" where
     5.1 --- a/src/ZF/Constructible/Relative.thy	Sun Apr 15 23:25:50 2007 +0200
     5.2 +++ b/src/ZF/Constructible/Relative.thy	Sun Apr 15 23:25:52 2007 +0200
     5.3 @@ -1431,12 +1431,12 @@
     5.4  
     5.5  definition
     5.6    is_Nil :: "[i=>o, i] => o" where
     5.7 -     --{* because @{term "[] \<equiv> Inl(0)"}*}
     5.8 +     --{* because @{prop "[] \<equiv> Inl(0)"}*}
     5.9      "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
    5.10  
    5.11  definition
    5.12    is_Cons :: "[i=>o,i,i,i] => o" where
    5.13 -     --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
    5.14 +     --{* because @{prop "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
    5.15      "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
    5.16  
    5.17  
     6.1 --- a/src/ZF/OrderArith.thy	Sun Apr 15 23:25:50 2007 +0200
     6.2 +++ b/src/ZF/OrderArith.thy	Sun Apr 15 23:25:52 2007 +0200
     6.3 @@ -369,7 +369,7 @@
     6.4  done
     6.5  
     6.6  text{*But note that the combination of @{text wf_imp_wf_on} and
     6.7 - @{text wf_rvimage} gives @{term "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
     6.8 + @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}*}
     6.9  lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
    6.10  apply (rule wf_onI2)
    6.11  apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba")
     7.1 --- a/src/ZF/WF.thy	Sun Apr 15 23:25:50 2007 +0200
     7.2 +++ b/src/ZF/WF.thy	Sun Apr 15 23:25:52 2007 +0200
     7.3 @@ -84,7 +84,7 @@
     7.4  
     7.5  text{*If @{term r} allows well-founded induction over @{term A}
     7.6     then we have @{term "wf[A](r)"}.   Premise is equivalent to
     7.7 -  @{term "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
     7.8 +  @{prop "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
     7.9  lemma wf_onI2:
    7.10   assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A |]
    7.11                         ==> y:B"