# HG changeset patch
# User nipkow
# Date 1456246043 -3600
# Node ID 747d36865c2c2387a69f0219785a6c3c8b08ebd4
# Parent  1658fc9b2618a1d7d7a4332e37546333a429b9d7
more canonical names

diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -1086,9 +1086,9 @@
   For technical reasons, there is a distinction between case splitting
   in the conclusion and in the premises of a subgoal.  The former is
   done by @{ML Splitter.split_tac} with rules like @{thm [source]
-  split_if} or @{thm [source] option.split}, which do not split the
+  if_split} or @{thm [source] option.split}, which do not split the
   subgoal, while the latter is done by @{ML Splitter.split_asm_tac}
-  with rules like @{thm [source] split_if_asm} or @{thm [source]
+  with rules like @{thm [source] if_split_asm} or @{thm [source]
   option.split_asm}, which split the subgoal.  The function @{ML
   Splitter.add_split} automatically takes care of which tactic to
   call, analyzing the form of the rules given as argument; it is the
diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Tutorial/Fun/fun0.thy
--- a/src/Doc/Tutorial/Fun/fun0.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Fun/fun0.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -137,7 +137,7 @@
 different ways.
 
 The most radical solution is to disable the offending theorem
-@{thm[source]split_if},
+@{thm[source]if_split},
 as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
 approach: you will often have to invoke the rule explicitly when
 @{text "if"} is involved.
diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Tutorial/Misc/simp.thy
--- a/src/Doc/Tutorial/Misc/simp.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Misc/simp.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -268,11 +268,11 @@
 The goal can be split by a special method, \methdx{split}:
 *}
 
-apply(split split_if)
+apply(split if_split)
 
 txt{*\noindent
 @{subgoals[display,indent=0]}
-where \tdx{split_if} is a theorem that expresses splitting of
+where \tdx{if_split} is a theorem that expresses splitting of
 @{text"if"}s. Because
 splitting the @{text"if"}s is usually the right proof strategy, the
 simplifier does it automatically.  Try \isacommand{apply}@{text"(simp)"}
@@ -316,7 +316,7 @@
 (*<*)
 lemma "dummy=dummy"
 (*>*)
-apply(simp split del: split_if)
+apply(simp split del: if_split)
 (*<*)
 oops
 (*>*)
@@ -334,11 +334,11 @@
 
 The split rules shown above are intended to affect only the subgoal's
 conclusion.  If you want to split an @{text"if"} or @{text"case"}-expression
-in the assumptions, you have to apply \tdx{split_if_asm} or
+in the assumptions, you have to apply \tdx{if_split_asm} or
 $t$@{text".split_asm"}: *}
 
 lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
-apply(split split_if_asm)
+apply(split if_split_asm)
 
 txt{*\noindent
 Unlike splitting the conclusion, this step creates two
diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -383,4 +383,4 @@
 
 (*<*)
 end
-(*>*)
\ No newline at end of file
+(*>*)
diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -483,7 +483,7 @@
 by (intro equalityI lemma1 lemma2)
 
 text{*Case analysis: either the message is secure, or it is not! Effective,
-but can cause subgoals to blow up! Use with @{text "split_if"}; apparently
+but can cause subgoals to blow up! Use with @{text "if_split"}; apparently
 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert
 (Crypt K X) H)"} *} 
 lemma analz_Crypt_if [simp]:
@@ -918,4 +918,4 @@
 
 
 end
-(*>*)
\ No newline at end of file
+(*>*)
diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Tutorial/Protocol/Public.thy
--- a/src/Doc/Tutorial/Protocol/Public.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Protocol/Public.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -169,4 +169,4 @@
     "for proving possibility theorems"
 
 end
-(*>*)
\ No newline at end of file
+(*>*)
diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Tutorial/Recdef/simplification.thy
--- a/src/Doc/Tutorial/Recdef/simplification.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Recdef/simplification.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -40,7 +40,7 @@
 different ways.
 
 The most radical solution is to disable the offending theorem
-@{thm[source]split_if},
+@{thm[source]if_split},
 as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
 approach: you will often have to invoke the rule explicitly when
 @{text "if"} is involved.
diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Tutorial/Types/Setup.thy
--- a/src/Doc/Tutorial/Types/Setup.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Types/Setup.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -5,4 +5,4 @@
 ML_file "../../antiquote_setup.ML"
 ML_file "../../more_antiquote.ML"
 
-end
\ No newline at end of file
+end