src/HOL/Bali/Basis.thy
changeset 24019 67bde7cfcf10
parent 22781 18fbba942a80
child 24038 18182c4aec9e
     1.1 --- a/src/HOL/Bali/Basis.thy	Sat Jul 28 20:40:20 2007 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sat Jul 28 20:40:22 2007 +0200
     1.3 @@ -11,22 +11,13 @@
     1.4  Unify.search_bound := 40;
     1.5  Unify.trace_bound  := 40;
     1.6  *}
     1.7 -(*print_depth 100;*)
     1.8 -(*Syntax.ambiguity_level := 1;*)
     1.9  
    1.10  section "misc"
    1.11  
    1.12  declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
    1.13  
    1.14 -ML {*
    1.15 -fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.theory_of_thm thm) name [pat]
    1.16 -  (fn _ => fn _ => fn t => if pred t then NONE else SOME (mk_meta_eq thm));
    1.17 -*}
    1.18 -
    1.19  declare split_if_asm  [split] option.split [split] option.split_asm [split]
    1.20 -ML {*
    1.21 -change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
    1.22 -*}
    1.23 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.24  declare if_weak_cong [cong del] option.weak_case_cong [cong del]
    1.25  declare length_Suc_conv [iff]
    1.26