clarified order of rules;
authorwenzelm
Sat Aug 16 19:01:31 2014 +0200 (2014-08-16)
changeset 57958045c96e3edf0
parent 57957 e6ee35b8f4b5
child 57959 1bfed12a7646
clarified order of rules;
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 18:31:47 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 19:01:31 2014 +0200
     1.3 @@ -517,7 +517,7 @@
     1.4          val DEFL_simps =
     1.5            Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
     1.6          fun tac ctxt =
     1.7 -          rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
     1.8 +          rewrite_goals_tac ctxt (map mk_meta_eq (rev DEFL_simps))
     1.9            THEN TRY (resolve_tac defl_unfold_thms 1)
    1.10        in
    1.11          Goal.prove_global thy [] [] goal (tac o #context)
    1.12 @@ -620,7 +620,7 @@
    1.13          val isodefl_rules =
    1.14            @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
    1.15            @ isodefl_abs_rep_thms
    1.16 -          @ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl}
    1.17 +          @ rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl})
    1.18        in
    1.19          Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
    1.20           EVERY
    1.21 @@ -632,7 +632,7 @@
    1.22             simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,
    1.23             simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1,
    1.24             REPEAT (etac @{thm conjE} 1),
    1.25 -           REPEAT (resolve_tac (rev isodefl_rules @ prems) 1 ORELSE atac 1)])
    1.26 +           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
    1.27        end
    1.28      val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
    1.29      fun conjuncts [] _ = []