src/Doc/IsarRef/ML_Tactic.thy
changeset 51304 0e71a248cacb
parent 50068 310e9b810bbf
child 51717 9e7d1c139569
equal deleted inserted replaced
51303:4cca272150ab 51304:0e71a248cacb
   117 
   117 
   118   \medskip
   118   \medskip
   119   \begin{tabular}{lll}
   119   \begin{tabular}{lll}
   120     @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\
   120     @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\
   121     @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\
   121     @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\
   122     @{ML strip_tac}~@{text 1} & @{text "\<approx>"} & @{text "intro strip"} \\
       
   123     @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
   122     @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
   124       & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
   123       & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
   125       & @{text "\<lless>"} & @{text "clarify"} \\
   124       & @{text "\<lless>"} & @{text "clarify"} \\
   126   \end{tabular}
   125   \end{tabular}
   127 *}
   126 *}