--- a/src/HOL/Import/proof_kernel.ML Fri Sep 23 09:00:19 2005 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Sep 23 10:01:14 2005 +0200
@@ -1009,7 +1009,6 @@
fun mk_GEN v th sg =
let
- val _ = writeln "enter mk_GEN"
val c = HOLogic.dest_Trueprop (concl_of th)
val cv = cterm_of sg v
val lc = Term.lambda v c
@@ -1027,7 +1026,6 @@
| _ => raise ERR "mk_GEN" "Unknown conclusion"
val th4 = Thm.rename_boundvars cold cnew th3
val res = implies_intr_hyps th4
- val _ = writeln "exit mk_GEN"
in
res
end
@@ -1198,7 +1196,6 @@
case get_hol4_mapping thyname thmname thy of
SOME (SOME thmname) =>
let
- val _ = writeln "isabelle_thm: SOME SOME"
val _ = message ("Looking for " ^ thmname)
val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
handle ERROR_MESSAGE _ =>
@@ -1217,14 +1214,13 @@
| SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
| NONE =>
let
- val _ = writeln "isabelle_thm: None"
val _ = (message "Looking for conclusion:";
if_debug prin isaconc)
val cs = non_trivial_term_consts isaconc
val _ = (message "Looking for consts:";
message (commas cs))
val pot_thms = Shuffler.find_potential thy isaconc
- val _ = writeln ((Int.toString (length pot_thms)) ^ " potential theorems")
+ val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
in
case Shuffler.set_prop thy isaconc pot_thms of
SOME (isaname,th) =>
@@ -1242,7 +1238,6 @@
fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
let
- val _ = writeln "enter get_isabelle_thm_and_warn"
val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
fun warn () =
let
@@ -1261,13 +1256,13 @@
end
in
case b of
- NONE => (warn () handle _ => (); writeln "exit get_isabelle_thm_and_warn"; (a,b))
- | _ => (writeln "exit get_isabelle_thm_and_warn"; (a, b))
+ NONE => (warn () handle _ => (); (a,b))
+ | _ => (a, b)
end
fun get_thm thyname thmname thy =
case get_hol4_thm thyname thmname thy of
- SOME hth => (writeln "got hol4 thm"; (thy,SOME hth))
+ SOME hth => (thy,SOME hth)
| NONE => ((case import_proof_concl thyname thmname thy of
SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
| NONE => (message "No conclusion"; (thy,NONE)))
@@ -1647,7 +1642,7 @@
fun GEN v hth thy =
let
- val _ = writeln "GEN:"
+ val _ = message "GEN:"
val _ = if_debug prin v
val _ = if_debug pth hth
val (info,th) = disamb_thm hth
@@ -1655,7 +1650,6 @@
val res = HOLThm(rens_of info',mk_GEN v' th (sign_of thy))
val _ = message "RESULT:"
val _ = if_debug pth res
- val _ = writeln "exit GEN"
in
(thy,res)
end
@@ -2082,6 +2076,14 @@
add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy
end
+fun add_dump_syntax thy name =
+ let
+ val n = quotename name
+ val syn = Syntax.string_of_mixfix (mk_syn thy name)
+ in
+ add_dump ("syntax\n "^n^" :: _ "^syn) thy
+ end
+
(*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
fun choose_upon_replay_history thy s dth =
case Symtab.lookup (!type_intro_replay_history) s of
@@ -2147,20 +2149,20 @@
val proc_prop = if null tnames
then smart_string_of_cterm
else Library.setmp show_all_types true smart_string_of_cterm
- val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of sg c)) ^ " " ^
- (Syntax.string_of_mixfix tsyn) ^ " \n"^
- ( " apply (rule light_ex_imp_nonempty[where t="^(proc_prop (cterm_of sg t))^"]) \n")^
- (" by (import " ^ thyname ^ " " ^ thmname ^ ")")) thy4
- val isa_rep_name = "Rep_"^tycname
- val isa_abs_name = "Abs_"^tycname
- val isa_rep_name_def = isa_rep_name^"_symdest"
- val isa_abs_name_def = isa_abs_name^"_symdest"
- val thy = add_dump_constdefs thy (SOME isa_rep_name_def) rep_name isa_rep_name rep_ty
- val thy = add_dump_constdefs thy (SOME isa_abs_name_def) abs_name isa_abs_name abs_ty
+ val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
+ " = " ^ (proc_prop (cterm_of sg c)) ^ " " ^
+ (Syntax.string_of_mixfix tsyn) ^ " morphisms "^
+ (quote rep_name)^" "^(quote abs_name)^"\n"^
+ (" apply (rule light_ex_imp_nonempty[where t="^
+ (proc_prop (cterm_of sg t))^"])\n"^
+ (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
val str_aty = string_of_ctyp (ctyp_of thy aty)
- val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ " = typedef_hol2hollight [where a=\"a :: "^str_aty^"\" and r=r" ^
- " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^
- " ,\n simplified "^(quotename isa_rep_name_def)^" [symmetric] "^(quotename isa_abs_name_def)^" [symmetric]"^"]") thy
+ val thy = add_dump_syntax thy rep_name
+ val thy = add_dump_syntax thy abs_name
+ val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
+ " = typedef_hol2hollight \n"^
+ " [where a=\"a :: "^str_aty^"\" and r=r" ^
+ " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
val _ = message "RESULT:"
val _ = if_debug pth hth'
in
--- a/src/HOL/Import/replay.ML Fri Sep 23 09:00:19 2005 +0200
+++ b/src/HOL/Import/replay.ML Fri Sep 23 10:01:14 2005 +0200
@@ -77,11 +77,8 @@
end
| rp (PGen(prf,v)) thy =
let
- val _ = writeln "enter rp PGen"
val (thy',th) = rp' prf thy
- val _ = writeln "replayed inner proof"
val p = P.GEN v th thy'
- val _ = writeln "exit rp PGen"
in
p
end
@@ -229,7 +226,7 @@
else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
| NONE =>
(case P.get_thm thyname' thmname thy of
- (thy',SOME res) => (writeln "Found theorem, no replay necessary!"; (thy',res))
+ (thy',SOME res) => (thy',res)
| (thy',NONE) =>
if thyname' = thyname
then
@@ -304,13 +301,10 @@
let
fun replay_fact (thmname,thy) =
let
- val _ = writeln ("import_single_thm: Replaying " ^ thmname)
val prf = mk_proof PDisk
- val _ = writeln ("Made proof.")
val _ = set_disk_info_of prf thyname thmname
- val _ = writeln ("set disk info")
+ val _ = writeln ("Replaying "^thmname^" ...")
val p = fst (replay_proof int_thms thyname thmname prf thy)
- val _ = writeln ("exit replay_fact")
in
p
end
@@ -322,13 +316,10 @@
let
fun replay_fact (thy,thmname) =
let
- val _ = writeln ("import_thms: Replaying " ^ thmname)
val prf = mk_proof PDisk
- val _ = writeln ("Made proof.")
- val _ = set_disk_info_of prf thyname thmname
- val _ = writeln ("set disk info")
+ val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("Replaying "^thmname^" ...")
val p = fst (replay_proof int_thms thyname thmname prf thy)
- val _ = writeln ("exit replay_fact")
in
p
end
@@ -342,13 +333,10 @@
val int_thms = fst (setup_int_thms thyname thy)
fun replay_fact (thmname,thy) =
let
- val _ = writeln ("import_thm: Replaying " ^ thmname)
val prf = mk_proof PDisk
- val _ = writeln ("Made proof.")
- val _ = set_disk_info_of prf thyname thmname
- val _ = writeln ("set disk info")
+ val _ = set_disk_info_of prf thyname thmname
+ val _ = writeln ("Replaying "^thmname^" ...")
val p = fst (replay_proof int_thms thyname thmname prf thy)
- val _ = writeln ("exit replay_fact")
in
p
end