--- a/src/HOL/IsaMakefile Mon Jul 31 14:33:40 2000 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 31 14:37:18 2000 +0200
@@ -498,16 +498,18 @@
## clean
clean:
- @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
- $(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
- $(LOG)/HOL-Induct.gz $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
- $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
- $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
- $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \
- $(LOG)/HOL-AxClasses-Group.gz \
- $(LOG)/HOL-AxClasses-Lattice.gz \
- $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \
- $(LOG)/HOL-ex.gz $(LOG)/HOL-Isar_examples.gz $(OUT)/TLA \
- $(LOG)/TLA.gz $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
- $(LOG)/TLA-Memory.gz $(LOG)/HOL-Real.gz $(LOG)/HOL-Real-ex.gz \
- $(LOG)/HOL-Real-HahnBanach.gz
+ @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
+ $(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
+ $(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
+ $(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
+ $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
+ $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
+ $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
+ $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
+ $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
+ $(LOG)/HOL-BCV.gz $(LOG)/HOL-MicroJava.gz \
+ $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses-Group.gz \
+ $(LOG)/HOL-AxClasses-Lattice.gz \
+ $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Real-ex.gz \
+ $(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
+ $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz
--- a/src/Pure/Isar/obtain.ML Mon Jul 31 14:33:40 2000 +0200
+++ b/src/Pure/Isar/obtain.ML Mon Jul 31 14:37:18 2000 +0200
@@ -38,7 +38,7 @@
struct
-(** export_obtained **)
+(** disch_obtained **)
fun disch_obtained state parms rule cprops thm =
let
@@ -55,16 +55,13 @@
val bads = parms inter (Term.term_frees concl);
in
if not (null bads) then
- raise Proof.STATE ("Result contains illegal parameters: " ^
+ raise Proof.STATE ("Conclusion contains obtained parameters: " ^
space_implode " " (map (Sign.string_of_term sign) bads), state)
else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
- raise Proof.STATE ("Conclusion of result is not an object-logic judgment", state)
+ raise Proof.STATE ("Conclusion is not an object-logic judgment", state)
else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
end;
-fun export_obtained state parms rule =
- (disch_obtained state parms rule, fn _ => fn _ => []);
-
(** obtain(_i) **)
@@ -108,11 +105,14 @@
val bound_thesis = bind_skolem (Data.atomic_thesis thesisN);
val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
+ fun export_obtained rule =
+ (disch_obtained state parms rule, fn _ => fn _ => []);
+
fun after_qed st = st
|> Proof.end_block
|> Seq.map (fn st' => st'
|> Proof.fix_i vars
- |> Proof.assm_i (export_obtained state parms (Proof.the_fact st')) asms);
+ |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
in
state
|> Proof.enter_forward