src/HOL/HOL.thy
changeset 16019 0e1405402d53
parent 15801 d2f5ca3c048d
child 16121 a80aa66d2271
equal deleted inserted replaced
16018:3e4e077af2e7 16019:0e1405402d53
  1122   by (unfold Let_def)
  1122   by (unfold Let_def)
  1123 
  1123 
  1124 subsubsection {* Actual Installation of the Simplifier *}
  1124 subsubsection {* Actual Installation of the Simplifier *}
  1125 
  1125 
  1126 use "simpdata.ML"
  1126 use "simpdata.ML"
  1127 setup Simplifier.setup
       
  1128 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
  1127 setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
  1129 setup Splitter.setup setup Clasimp.setup
  1128 setup Splitter.setup setup Clasimp.setup
  1130 
  1129 
  1131 
  1130 
  1132 subsubsection {* Lucas Dixon's eqstep tactic *}
  1131 subsubsection {* Lucas Dixon's eqstep tactic *}