equal
deleted
inserted
replaced
1404 The most common combinators for modifying simpsets are: |
1404 The most common combinators for modifying simpsets are: |
1405 |
1405 |
1406 \begin{isabelle} |
1406 \begin{isabelle} |
1407 \begin{tabular}{l@ {\hspace{10mm}}l} |
1407 \begin{tabular}{l@ {\hspace{10mm}}l} |
1408 @{ML_ind addsimps in Raw_Simplifier} & @{ML_ind delsimps in Raw_Simplifier}\\ |
1408 @{ML_ind addsimps in Raw_Simplifier} & @{ML_ind delsimps in Raw_Simplifier}\\ |
1409 @{ML_ind addcongs in Raw_Simplifier} & @{ML_ind delcongs in Raw_Simplifier}\\ |
|
1410 @{ML_ind addsimprocs in Raw_Simplifier} & @{ML_ind delsimprocs in Raw_Simplifier}\\ |
1409 @{ML_ind addsimprocs in Raw_Simplifier} & @{ML_ind delsimprocs in Raw_Simplifier}\\ |
|
1410 @{ML_ind add_cong in Raw_Simplifier} & @{ML_ind del_cong in Raw_Simplifier}\\ |
1411 \end{tabular} |
1411 \end{tabular} |
1412 \end{isabelle} |
1412 \end{isabelle} |
1413 |
1413 |
1414 \footnote{\bf FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}} |
|
1415 *} |
1414 *} |
1416 |
1415 |
1417 text_raw {* |
1416 text_raw {* |
1418 \begin{figure}[t] |
1417 \begin{figure}[t] |
1419 \begin{minipage}{\textwidth} |
1418 \begin{minipage}{\textwidth} |
1474 \footnote{\bf FIXME: Why does it print out ??.unknown} |
1473 \footnote{\bf FIXME: Why does it print out ??.unknown} |
1475 |
1474 |
1476 Adding also the congruence rule @{thm [source] UN_cong} |
1475 Adding also the congruence rule @{thm [source] UN_cong} |
1477 *} |
1476 *} |
1478 |
1477 |
1479 ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *} |
1478 ML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *} |
1480 |
1479 |
1481 text {* |
1480 text {* |
1482 gives |
1481 gives |
1483 |
1482 |
1484 @{ML_response_fake [display,gray] |
1483 @{ML_response_fake [display,gray] |