'also'/'moreover': do not interfere with current facts, allow in chain mode;
authorwenzelm
Tue Apr 13 20:22:26 2004 +0200 (2004-04-13)
changeset 14555341908d6c792
parent 14554 b9cd48af3512
child 14556 c5078f6c99a9
'also'/'moreover': do not interfere with current facts, allow in chain mode;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Tue Apr 13 20:21:11 2004 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Tue Apr 13 20:22:26 2004 +0200
     1.3 @@ -134,18 +134,18 @@
     1.4  
     1.5  (** proof commands **)
     1.6  
     1.7 +fun assert_sane final =
     1.8 +  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
     1.9 +
    1.10 +
    1.11  (* maintain calculation register *)
    1.12  
    1.13  val calculationN = "calculation";
    1.14  
    1.15  fun maintain_calculation false calc state =
    1.16 -    let val facts = Proof.the_facts state 
    1.17 -    in
    1.18        state
    1.19        |> put_calculation calc
    1.20 -      |> Proof.simple_have_thms calculationN calc
    1.21 -      |> Proof.simple_have_thms Proof.thisN facts
    1.22 -    end
    1.23 +      |> Proof.put_thms (calculationN, calc)
    1.24    | maintain_calculation true calc state =
    1.25        state
    1.26        |> reset_calculation
    1.27 @@ -172,7 +172,7 @@
    1.28        |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
    1.29        |> Seq.filter (not o projection ths);
    1.30  
    1.31 -    val facts = Proof.the_facts (Proof.assert_forward state);
    1.32 +    val facts = Proof.the_facts (assert_sane final state);
    1.33      val (initial, calculations) =
    1.34        (case get_calculation state of
    1.35          None => (true, Seq.single facts)
    1.36 @@ -192,7 +192,7 @@
    1.37  
    1.38  fun collect final print state =
    1.39    let
    1.40 -    val facts = Proof.the_facts (Proof.assert_forward state);
    1.41 +    val facts = Proof.the_facts (assert_sane final state);
    1.42      val (initial, thms) =
    1.43        (case get_calculation state of
    1.44          None => (true, [])