--- a/src/HOL/Complex/ROOT.ML Wed Nov 29 15:44:56 2006 +0100
+++ b/src/HOL/Complex/ROOT.ML Wed Nov 29 15:44:57 2006 +0100
@@ -2,7 +2,7 @@
ID: $Id$
Author: Jacques Fleuriot
-The Complex Numbers
+The Complex Numbers.
*)
no_document use_thy "Infinite_Set";
@@ -10,4 +10,4 @@
with_path "../Real" use_thy "Float";
with_path "../Hyperreal" use_thy "Hyperreal";
-time_use_thy "Complex_Main";
+use_thy "Complex_Main";
--- a/src/HOL/Import/import_package.ML Wed Nov 29 15:44:56 2006 +0100
+++ b/src/HOL/Import/import_package.ML Wed Nov 29 15:44:57 2006 +0100
@@ -38,47 +38,47 @@
else
fn thy =>
fn th =>
- let
+ let
val sg = sign_of_thm th
- val prem = hd (prems_of th)
+ val prem = hd (prems_of th)
val _ = message ("Import_tac: thyname="^thyname^", thmname="^thmname)
- val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
- val int_thms = case ImportData.get thy of
- NONE => fst (Replay.setup_int_thms thyname thy)
- | SOME a => a
- val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
- val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
- val thm = snd (ProofKernel.to_isa_thm hol4thm)
- val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
- val thm = equal_elim rew thm
- val prew = ProofKernel.rewrite_hol4_term prem thy
- val prem' = #2 (Logic.dest_equals (prop_of prew))
- val _ = message ("Import proved " ^ (string_of_thm thm))
+ val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
+ val int_thms = case ImportData.get thy of
+ NONE => fst (Replay.setup_int_thms thyname thy)
+ | SOME a => a
+ val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
+ val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
+ val thm = snd (ProofKernel.to_isa_thm hol4thm)
+ val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
+ val thm = equal_elim rew thm
+ val prew = ProofKernel.rewrite_hol4_term prem thy
+ val prem' = #2 (Logic.dest_equals (prop_of prew))
+ val _ = message ("Import proved " ^ (string_of_thm thm))
val thm = ProofKernel.disambiguate_frees thm
- val _ = message ("Disambiguate: " ^ (string_of_thm thm))
- in
- case Shuffler.set_prop thy prem' [("",thm)] of
- SOME (_,thm) =>
- let
- val _ = if prem' aconv (prop_of thm)
- then message "import: Terms match up"
- else message "import: Terms DO NOT match up"
- val thm' = equal_elim (symmetric prew) thm
- val res = bicompose true (false,thm',0) 1 th
- in
- res
- end
- | NONE => (message "import: set_prop didn't succeed"; no_tac th)
- end
-
+ val _ = message ("Disambiguate: " ^ (string_of_thm thm))
+ in
+ case Shuffler.set_prop thy prem' [("",thm)] of
+ SOME (_,thm) =>
+ let
+ val _ = if prem' aconv (prop_of thm)
+ then message "import: Terms match up"
+ else message "import: Terms DO NOT match up"
+ val thm' = equal_elim (symmetric prew) thm
+ val res = bicompose true (false,thm',0) 1 th
+ in
+ res
+ end
+ | NONE => (message "import: set_prop didn't succeed"; no_tac th)
+ end
+
val import_meth = Method.simple_args (Args.name -- Args.name)
- (fn arg =>
- fn ctxt =>
- let
- val thy = ProofContext.theory_of ctxt
- in
- Method.SIMPLE_METHOD (import_tac arg thy)
- end)
+ (fn arg =>
+ fn ctxt =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ in
+ Method.SIMPLE_METHOD (import_tac arg thy)
+ end)
val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
end
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Wed Nov 29 15:44:56 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Wed Nov 29 15:44:57 2006 +0100
@@ -205,7 +205,7 @@
end
(* the main function: create table, search table, create relation,
- and prove the subgoals *)
+ and prove the subgoals *) (* FIXME proper goal addressing -- do not hardwire 1 *)
fun lexicographic_order_tac ctxt (st: thm) =
let
val thy = theory_of_thm st
@@ -248,4 +248,4 @@
val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")]
-end
\ No newline at end of file
+end
--- a/src/Sequents/S4.thy Wed Nov 29 15:44:56 2006 +0100
+++ b/src/Sequents/S4.thy Wed Nov 29 15:44:57 2006 +0100
@@ -45,7 +45,7 @@
*}
method_setup S4_solve =
-{* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
+ {* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
--- a/src/Sequents/T.thy Wed Nov 29 15:44:56 2006 +0100
+++ b/src/Sequents/T.thy Wed Nov 29 15:44:57 2006 +0100
@@ -44,7 +44,7 @@
*}
method_setup T_solve =
-{* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
+ {* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)