# HG changeset patch # User wenzelm # Date 1164811497 -3600 # Node ID ef7278f553eb9801f7ff187233f7f0282fb2bb8c # Parent 1b02201d71952caf82cb255cfbecee4fdfc653d4 tuned spaces/comments; diff -r 1b02201d7195 -r ef7278f553eb src/HOL/Complex/ROOT.ML --- 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"; diff -r 1b02201d7195 -r ef7278f553eb src/HOL/Import/import_package.ML --- 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 diff -r 1b02201d7195 -r ef7278f553eb src/HOL/Tools/function_package/lexicographic_order.ML --- 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 diff -r 1b02201d7195 -r ef7278f553eb src/Sequents/S4.thy --- 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 *) diff -r 1b02201d7195 -r ef7278f553eb src/Sequents/T.thy --- 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 *)