src/HOL/Bali/Basis.thy
changeset 51304 0e71a248cacb
parent 45151 2dd44cd8f963
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Feb 28 13:19:25 2013 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Feb 28 13:24:51 2013 +0100
     1.3 @@ -9,6 +9,8 @@
     1.4  
     1.5  section "misc"
     1.6  
     1.7 +ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
     1.8 +
     1.9  declare split_if_asm  [split] option.split [split] option.split_asm [split]
    1.10  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.11  declare if_weak_cong [cong del] option.weak_case_cong [cong del]