src/Doc/Isar_Ref/Generic.thy
changeset 61424 c3658c18b7bc
parent 61421 e0825405d398
child 61439 2bf52eec4e8a
     1.1 --- a/src/Doc/Isar_Ref/Generic.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -1130,9 +1130,9 @@
     1.4    @{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"}
     1.5  
     1.6    Another example is the elimination operator for Cartesian products
     1.7 -  (which happens to be called @{text split} in Isabelle/HOL:
     1.8 +  (which happens to be called @{const case_prod} in Isabelle/HOL:
     1.9  
    1.10 -  @{text [display] "?P (split ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
    1.11 +  @{text [display] "?P (case_prod ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
    1.12  
    1.13    For technical reasons, there is a distinction between case splitting
    1.14    in the conclusion and in the premises of a subgoal.  The former is