tuned spaces/comments;
authorwenzelm
Wed Nov 29 15:44:57 2006 +0100 (2006-11-29)
changeset 21590ef7278f553eb
parent 21589 1b02201d7195
child 21591 5e0f2340caa7
tuned spaces/comments;
src/HOL/Complex/ROOT.ML
src/HOL/Import/import_package.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/Sequents/S4.thy
src/Sequents/T.thy
     1.1 --- a/src/HOL/Complex/ROOT.ML	Wed Nov 29 15:44:56 2006 +0100
     1.2 +++ b/src/HOL/Complex/ROOT.ML	Wed Nov 29 15:44:57 2006 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Jacques Fleuriot
     1.6  
     1.7 -The Complex Numbers
     1.8 +The Complex Numbers.
     1.9  *)
    1.10  
    1.11  no_document use_thy "Infinite_Set";
    1.12 @@ -10,4 +10,4 @@
    1.13  
    1.14  with_path "../Real" use_thy "Float";
    1.15  with_path "../Hyperreal" use_thy "Hyperreal";
    1.16 -time_use_thy "Complex_Main";
    1.17 +use_thy "Complex_Main";
     2.1 --- a/src/HOL/Import/import_package.ML	Wed Nov 29 15:44:56 2006 +0100
     2.2 +++ b/src/HOL/Import/import_package.ML	Wed Nov 29 15:44:57 2006 +0100
     2.3 @@ -38,47 +38,47 @@
     2.4      else
     2.5       fn thy =>
     2.6       fn th =>
     2.7 -	let
     2.8 +        let
     2.9              val sg = sign_of_thm th
    2.10 -	    val prem = hd (prems_of th)
    2.11 +            val prem = hd (prems_of th)
    2.12              val _ = message ("Import_tac: thyname="^thyname^", thmname="^thmname)
    2.13 -	    val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
    2.14 -	    val int_thms = case ImportData.get thy of
    2.15 -			       NONE => fst (Replay.setup_int_thms thyname thy)
    2.16 -			     | SOME a => a
    2.17 -	    val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
    2.18 -	    val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
    2.19 -	    val thm = snd (ProofKernel.to_isa_thm hol4thm)
    2.20 -	    val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
    2.21 -	    val thm = equal_elim rew thm
    2.22 -	    val prew = ProofKernel.rewrite_hol4_term prem thy
    2.23 -	    val prem' = #2 (Logic.dest_equals (prop_of prew))
    2.24 -            val _ = message ("Import proved " ^ (string_of_thm thm))    
    2.25 +            val _ = message ("Import trying to prove " ^ (string_of_cterm (cterm_of sg prem)))
    2.26 +            val int_thms = case ImportData.get thy of
    2.27 +                               NONE => fst (Replay.setup_int_thms thyname thy)
    2.28 +                             | SOME a => a
    2.29 +            val proof = snd (ProofKernel.import_proof thyname thmname thy) thy
    2.30 +            val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
    2.31 +            val thm = snd (ProofKernel.to_isa_thm hol4thm)
    2.32 +            val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
    2.33 +            val thm = equal_elim rew thm
    2.34 +            val prew = ProofKernel.rewrite_hol4_term prem thy
    2.35 +            val prem' = #2 (Logic.dest_equals (prop_of prew))
    2.36 +            val _ = message ("Import proved " ^ (string_of_thm thm))
    2.37              val thm = ProofKernel.disambiguate_frees thm
    2.38 -	    val _ = message ("Disambiguate: " ^ (string_of_thm thm))  
    2.39 -	in
    2.40 -	    case Shuffler.set_prop thy prem' [("",thm)] of
    2.41 -		SOME (_,thm) =>
    2.42 -		let
    2.43 -		    val _ = if prem' aconv (prop_of thm)
    2.44 -			    then message "import: Terms match up"
    2.45 -			    else message "import: Terms DO NOT match up"
    2.46 -		    val thm' = equal_elim (symmetric prew) thm
    2.47 -		    val res = bicompose true (false,thm',0) 1 th
    2.48 -		in
    2.49 -		    res
    2.50 -		end
    2.51 -	      | NONE => (message "import: set_prop didn't succeed"; no_tac th)
    2.52 -	end
    2.53 -	
    2.54 +            val _ = message ("Disambiguate: " ^ (string_of_thm thm))
    2.55 +        in
    2.56 +            case Shuffler.set_prop thy prem' [("",thm)] of
    2.57 +                SOME (_,thm) =>
    2.58 +                let
    2.59 +                    val _ = if prem' aconv (prop_of thm)
    2.60 +                            then message "import: Terms match up"
    2.61 +                            else message "import: Terms DO NOT match up"
    2.62 +                    val thm' = equal_elim (symmetric prew) thm
    2.63 +                    val res = bicompose true (false,thm',0) 1 th
    2.64 +                in
    2.65 +                    res
    2.66 +                end
    2.67 +              | NONE => (message "import: set_prop didn't succeed"; no_tac th)
    2.68 +        end
    2.69 +
    2.70  val import_meth = Method.simple_args (Args.name -- Args.name)
    2.71 -		  (fn arg =>
    2.72 -		   fn ctxt =>
    2.73 -		      let
    2.74 -			  val thy = ProofContext.theory_of ctxt
    2.75 -		      in
    2.76 -			  Method.SIMPLE_METHOD (import_tac arg thy)
    2.77 -		      end)
    2.78 +                  (fn arg =>
    2.79 +                   fn ctxt =>
    2.80 +                      let
    2.81 +                          val thy = ProofContext.theory_of ctxt
    2.82 +                      in
    2.83 +                          Method.SIMPLE_METHOD (import_tac arg thy)
    2.84 +                      end)
    2.85  
    2.86  val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
    2.87  end
     3.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Nov 29 15:44:56 2006 +0100
     3.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Nov 29 15:44:57 2006 +0100
     3.3 @@ -205,7 +205,7 @@
     3.4      end
     3.5        
     3.6  (* the main function: create table, search table, create relation,
     3.7 -   and prove the subgoals *)
     3.8 +   and prove the subgoals *)  (* FIXME proper goal addressing -- do not hardwire 1 *)
     3.9  fun lexicographic_order_tac ctxt (st: thm) = 
    3.10      let
    3.11        val thy = theory_of_thm st
    3.12 @@ -248,4 +248,4 @@
    3.13  
    3.14  val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")]
    3.15  
    3.16 -end
    3.17 \ No newline at end of file
    3.18 +end
     4.1 --- a/src/Sequents/S4.thy	Wed Nov 29 15:44:56 2006 +0100
     4.2 +++ b/src/Sequents/S4.thy	Wed Nov 29 15:44:57 2006 +0100
     4.3 @@ -45,7 +45,7 @@
     4.4  *}
     4.5  
     4.6  method_setup S4_solve =
     4.7 -{* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
     4.8 +  {* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
     4.9  
    4.10  
    4.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
     5.1 --- a/src/Sequents/T.thy	Wed Nov 29 15:44:56 2006 +0100
     5.2 +++ b/src/Sequents/T.thy	Wed Nov 29 15:44:57 2006 +0100
     5.3 @@ -44,7 +44,7 @@
     5.4  *}
     5.5  
     5.6  method_setup T_solve =
     5.7 -{* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
     5.8 +  {* Method.no_args (Method.SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
     5.9  
    5.10  
    5.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)