equal
deleted
inserted
replaced
452 (*** integration of simplifier with classical reasoner ***) |
452 (*** integration of simplifier with classical reasoner ***) |
453 |
453 |
454 structure Clasimp = ClasimpFun |
454 structure Clasimp = ClasimpFun |
455 (structure Simplifier = Simplifier and Splitter = Splitter |
455 (structure Simplifier = Simplifier and Splitter = Splitter |
456 and Classical = Classical and Blast = Blast |
456 and Classical = Classical and Blast = Blast |
457 val dest_Trueprop = HOLogic.dest_Trueprop |
457 val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE |
458 val iff_const = HOLogic.eq_const HOLogic.boolT |
|
459 val not_const = HOLogic.not_const |
|
460 val notE = notE val iffD1 = iffD1 val iffD2 = iffD2 |
|
461 val cla_make_elim = cla_make_elim); |
458 val cla_make_elim = cla_make_elim); |
462 open Clasimp; |
459 open Clasimp; |
463 |
460 |
464 val HOL_css = (HOL_cs, HOL_ss); |
461 val HOL_css = (HOL_cs, HOL_ss); |
465 |
462 |