equal
deleted
inserted
replaced
581 |
581 |
582 subsection {* Initializing the fixrec package *} |
582 subsection {* Initializing the fixrec package *} |
583 |
583 |
584 use "Tools/fixrec_package.ML" |
584 use "Tools/fixrec_package.ML" |
585 |
585 |
|
586 setup {* FixrecPackage.setup *} |
|
587 |
|
588 setup {* |
|
589 FixrecPackage.add_matchers |
|
590 [ (@{const_name up}, @{const_name match_up}), |
|
591 (@{const_name sinl}, @{const_name match_sinl}), |
|
592 (@{const_name sinr}, @{const_name match_sinr}), |
|
593 (@{const_name spair}, @{const_name match_spair}), |
|
594 (@{const_name cpair}, @{const_name match_cpair}), |
|
595 (@{const_name ONE}, @{const_name match_ONE}), |
|
596 (@{const_name TT}, @{const_name match_TT}), |
|
597 (@{const_name FF}, @{const_name match_FF}) ] |
|
598 *} |
|
599 |
586 hide (open) const return bind fail run cases |
600 hide (open) const return bind fail run cases |
587 |
601 |
588 end |
602 end |