--- 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
--- 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.
--- 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
--- 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
+(*>*)
--- 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
+(*>*)
--- 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
+(*>*)
--- 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.
--- 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