tuned comments;
authorwenzelm
Tue Jan 31 18:19:25 2006 +0100 (2006-01-31)
changeset 18870020e242c02a0
parent 18869 00741f7280f7
child 18871 ca48320f6619
tuned comments;
src/Pure/Isar/obtain.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Jan 31 17:48:28 2006 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jan 31 18:19:25 2006 +0100
     1.3 @@ -8,15 +8,18 @@
     1.4  similar, but derives these elements from the course of reasoning!
     1.5  
     1.6    <chain_facts>
     1.7 -  obtain x where "P x" <proof> ==
     1.8 +  obtain x where "A x" <proof> ==
     1.9  
    1.10 -  have "!!thesis. (!!x. P x ==> thesis) ==> thesis"
    1.11 +  have "!!thesis. (!!x. A x ==> thesis) ==> thesis"
    1.12    proof succeed
    1.13      fix thesis
    1.14 -    assume that [intro?]: "!!x. P x ==> thesis"
    1.15 -    <chain_facts> show thesis <proof (insert that)>
    1.16 +    assume that [intro?]: "!!x. A x ==> thesis"
    1.17 +    <chain_facts>
    1.18 +    show thesis
    1.19 +      apply (insert that)
    1.20 +      <proof>
    1.21    qed
    1.22 -  fix x assm (obtained) "P x"
    1.23 +  fix x assm <<obtain_export>> "A x"
    1.24  
    1.25  
    1.26    <chain_facts>
    1.27 @@ -25,13 +28,13 @@
    1.28    {
    1.29      fix thesis
    1.30      <chain_facts> have "PROP ?guess"
    1.31 -      apply magic      -- {* turns goal into "thesis ==> Goal thesis" *}
    1.32 +      apply magic      -- {* turns goal into "thesis ==> #thesis" *}
    1.33        <proof body>
    1.34 -      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> Goal thesis" into
    1.35 -        "Goal ((!!x. P x ==> thesis) ==> thesis)" which is a finished goal state *}
    1.36 +      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
    1.37 +        "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
    1.38        <proof end>
    1.39    }
    1.40 -  fix x assm (obtained) "P x"
    1.41 +  fix x assm <<obtain_export>> "A x"
    1.42  *)
    1.43  
    1.44  signature OBTAIN =
    1.45 @@ -52,6 +55,14 @@
    1.46  
    1.47  (** obtain_export **)
    1.48  
    1.49 +(*
    1.50 +    [x]
    1.51 +    [A x]
    1.52 +      :
    1.53 +      B
    1.54 +    -----
    1.55 +      B
    1.56 +*)
    1.57  fun obtain_export ctxt parms rule cprops thm =
    1.58    let
    1.59      val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
    1.60 @@ -136,8 +147,7 @@
    1.61      |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
    1.62      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    1.63      |> Proof.fix_i [(thesisN, NONE)]
    1.64 -    |> Proof.assume_i
    1.65 -      [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
    1.66 +    |> Proof.assume_i [((thatN, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
    1.67      |> `Proof.the_facts
    1.68      ||> Proof.chain_facts chain_facts
    1.69      ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
     2.1 --- a/src/Pure/ROOT.ML	Tue Jan 31 17:48:28 2006 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Tue Jan 31 18:19:25 2006 +0100
     2.3 @@ -63,7 +63,7 @@
     2.4  use "Thy/thy_load.ML";
     2.5  use "Thy/thy_info.ML";
     2.6  
     2.7 -(*theory syntax -- new format*)
     2.8 +(*theory syntax*)
     2.9  use "Isar/outer_lex.ML";
    2.10  
    2.11  (*theory presentation*)