# HG changeset patch
# User nipkow
# Date 1456242074 -3600
# Node ID 1658fc9b2618a1d7d7a4332e37546333a429b9d7
# Parent  842917225d56c8133c685a3865a194c23c1d7e98
more canonical names

diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -261,4 +261,4 @@
   THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
   THEN gen_eval_tac (approximation_conv ctxt) ctxt i
     
-end;
\ No newline at end of file
+end;
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Decision_Procs/langford.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -260,4 +260,4 @@
       THEN Object_Logic.full_atomize_tac ctxt i
       THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
       THEN (simp_tac (put_simpset ss ctxt) i)));
-end;
\ No newline at end of file
+end;
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Matrix_LP/Compute_Oracle/report.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/report.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/report.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -30,4 +30,4 @@
 end
 
 end
-end
\ No newline at end of file
+end
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -365,4 +365,4 @@
 
 end;
 
-end;
\ No newline at end of file
+end;
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -32,8 +32,8 @@
 val atomize_conjL = @{thm atomize_conjL};
 val falseEs = @{thms not_TrueE FalseE};
 val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
-val split_if = @{thm split_if};
-val split_if_asm = @{thm split_if_asm};
+val if_split = @{thm if_split};
+val if_split_asm = @{thm if_split_asm};
 val split_connectI = @{thms allI impI conjI};
 val unfold_lets = @{thms Let_def[abs_def] split_beta}
 
@@ -136,8 +136,8 @@
   HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE'
     eresolve_tac ctxt falseEs ORELSE'
     resolve_tac ctxt split_connectI ORELSE'
-    Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
-    Splitter.split_tac ctxt (split_if :: splits) ORELSE'
+    Splitter.split_asm_tac ctxt (if_split_asm :: split_asms) ORELSE'
+    Splitter.split_tac ctxt (if_split :: splits) ORELSE'
     eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
     assume_tac ctxt ORELSE'
     etac ctxt notE THEN' assume_tac ctxt ORELSE'
@@ -169,7 +169,7 @@
 fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
   let
     val splits' =
-      map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits);
+      map (fn th => th RS iffD2) (@{thm if_split_eq2} :: map (inst_split_eq ctxt) splits);
   in
     HEADGOAL (REPEAT o (resolve_tac ctxt (splits' @ split_connectI))) THEN
     prelude_tac ctxt [] (fun_ctr RS trans) THEN
@@ -177,8 +177,8 @@
       SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
       (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
        resolve_tac ctxt (@{thm Code.abort_def} :: split_connectI) ORELSE'
-       Splitter.split_tac ctxt (split_if :: splits) ORELSE'
-       Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
+       Splitter.split_tac ctxt (if_split :: splits) ORELSE'
+       Splitter.split_asm_tac ctxt (if_split_asm :: split_asms) ORELSE'
        mk_primcorec_assumption_tac ctxt discIs ORELSE'
        distinct_in_prems_tac ctxt distincts ORELSE'
        (TRY o dresolve_tac ctxt discIs) THEN' etac ctxt notE THEN' assume_tac ctxt)))))
@@ -210,7 +210,7 @@
     SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
     (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
      resolve_tac ctxt split_connectI ORELSE'
-     Splitter.split_tac ctxt (split_if :: splits) ORELSE'
+     Splitter.split_tac ctxt (if_split :: splits) ORELSE'
      distinct_in_prems_tac ctxt distincts ORELSE'
      rtac ctxt sym THEN' assume_tac ctxt ORELSE'
      etac ctxt notE THEN' assume_tac ctxt));
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -477,4 +477,4 @@
     (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
     fun_names)
 
-end
\ No newline at end of file
+end
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Tools/Predicate_Compile/mode_inference.ML
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -544,4 +544,4 @@
     ((moded_clauses, need_random), errors)
   end;
 
-end;
\ No newline at end of file
+end;
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -320,7 +320,7 @@
       else all_tac
   in
     split_term_tac (HOLogic.mk_tuple out_ts)
-    THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt @{thms split_if_asm} 1)
+    THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt @{thms if_split_asm} 1)
     THEN (eresolve_tac ctxt @{thms botE} 2))))
   end
 
@@ -505,4 +505,4 @@
       else (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)))
   end
 
-end
\ No newline at end of file
+end
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -209,4 +209,4 @@
     fold_map specialise' specs thy
   end
 
-end
\ No newline at end of file
+end
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Tools/Quickcheck/abstract_generators.ML
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -75,4 +75,4 @@
       >> (fn ((tyco, opt_pred), constrs) =>
         Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs)))
 
-end;
\ No newline at end of file
+end;
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -412,4 +412,4 @@
      preferred_methss = preferred_methss, run_time = run_time, message = message}
   end
 
-end;
\ No newline at end of file
+end;
diff -r 842917225d56 -r 1658fc9b2618 src/HOL/Tools/boolean_algebra_cancel.ML
--- a/src/HOL/Tools/boolean_algebra_cancel.ML	Tue Feb 23 16:25:08 2016 +0100
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML	Tue Feb 23 16:41:14 2016 +0100
@@ -78,4 +78,4 @@
 val cancel_sup_conv = cancel_conv true (fn pos => if pos then mk_meta_eq @{thm sup_cancel_left1} else mk_meta_eq @{thm sup_cancel_left2})
 val cancel_inf_conv = cancel_conv false (fn pos => if pos then mk_meta_eq @{thm inf_cancel_left1} else mk_meta_eq @{thm inf_cancel_left2})
 
-end
\ No newline at end of file
+end