tuned;
authorwenzelm
Mon Jul 31 14:37:18 2000 +0200 (2000-07-31)
changeset 9481b16624f1ea38
parent 9480 7afb808b6b3e
child 9482 9c438a65be0a
tuned;
src/HOL/IsaMakefile
src/Pure/Isar/obtain.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Jul 31 14:33:40 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jul 31 14:37:18 2000 +0200
     1.3 @@ -498,16 +498,18 @@
     1.4  ## clean
     1.5  
     1.6  clean:
     1.7 -	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
     1.8 -	  $(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
     1.9 -	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    1.10 -	  $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.11 -	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.12 -	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \
    1.13 -	  $(LOG)/HOL-AxClasses-Group.gz		\
    1.14 -	  $(LOG)/HOL-AxClasses-Lattice.gz	\
    1.15 -	  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
    1.16 -	  $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
    1.17 -	  $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
    1.18 -	  $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Real-ex.gz \
    1.19 -	  $(LOG)/HOL-Real-HahnBanach.gz
    1.20 +	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
    1.21 +		$(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
    1.22 +		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
    1.23 +		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
    1.24 +		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
    1.25 +		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    1.26 +		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.27 +		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.28 +		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
    1.29 +		$(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
    1.30 +		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses-Group.gz \
    1.31 +		$(LOG)/HOL-AxClasses-Lattice.gz	\
    1.32 +		$(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Real-ex.gz \
    1.33 +		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
    1.34 +		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
     2.1 --- a/src/Pure/Isar/obtain.ML	Mon Jul 31 14:33:40 2000 +0200
     2.2 +++ b/src/Pure/Isar/obtain.ML	Mon Jul 31 14:37:18 2000 +0200
     2.3 @@ -38,7 +38,7 @@
     2.4  struct
     2.5  
     2.6  
     2.7 -(** export_obtained **)
     2.8 +(** disch_obtained **)
     2.9  
    2.10  fun disch_obtained state parms rule cprops thm =
    2.11    let
    2.12 @@ -55,16 +55,13 @@
    2.13      val bads = parms inter (Term.term_frees concl);
    2.14    in
    2.15      if not (null bads) then
    2.16 -      raise Proof.STATE ("Result contains illegal parameters: " ^
    2.17 +      raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    2.18          space_implode " " (map (Sign.string_of_term sign) bads), state)
    2.19      else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
    2.20 -      raise Proof.STATE ("Conclusion of result is not an object-logic judgment", state)
    2.21 +      raise Proof.STATE ("Conclusion is not an object-logic judgment", state)
    2.22      else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    2.23    end;
    2.24  
    2.25 -fun export_obtained state parms rule =
    2.26 -  (disch_obtained state parms rule, fn _ => fn _ => []);
    2.27 -
    2.28  
    2.29  
    2.30  (** obtain(_i) **)
    2.31 @@ -108,11 +105,14 @@
    2.32      val bound_thesis = bind_skolem (Data.atomic_thesis thesisN);
    2.33      val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
    2.34  
    2.35 +    fun export_obtained rule =
    2.36 +      (disch_obtained state parms rule, fn _ => fn _ => []);
    2.37 +
    2.38      fun after_qed st = st
    2.39        |> Proof.end_block
    2.40        |> Seq.map (fn st' => st'
    2.41          |> Proof.fix_i vars
    2.42 -        |> Proof.assm_i (export_obtained state parms (Proof.the_fact st')) asms);
    2.43 +        |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
    2.44    in
    2.45      state
    2.46      |> Proof.enter_forward