equal
deleted
inserted
replaced
423 by (asm_simp_tac HOL_ss 1); |
423 by (asm_simp_tac HOL_ss 1); |
424 qed "restrict_to_left"; |
424 qed "restrict_to_left"; |
425 |
425 |
426 (* default simpset *) |
426 (* default simpset *) |
427 val simpsetup = |
427 val simpsetup = |
428 [fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)]; |
428 (fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)); |
429 |
429 |
430 |
430 |
431 (*** integration of simplifier with classical reasoner ***) |
431 (*** integration of simplifier with classical reasoner ***) |
432 |
432 |
433 structure Clasimp = ClasimpFun |
433 structure Clasimp = ClasimpFun |