equal
deleted
inserted
replaced
1 theory Tactical |
1 theory Tactical |
2 imports Base FirstSteps |
2 imports Base First_Steps |
3 begin |
3 begin |
4 |
4 |
5 (*<*) |
5 (*<*) |
6 setup{* |
6 setup{* |
7 open_file_with_prelude |
7 open_file_with_prelude |
8 "Tactical_Code.thy" |
8 "Tactical_Code.thy" |
9 ["theory Tactical", "imports Base FirstSteps", "begin"] |
9 ["theory Tactical", "imports Base First_Steps", "begin"] |
10 *} |
10 *} |
11 (*>*) |
11 (*>*) |
12 |
12 |
13 chapter {* Tactical Reasoning\label{chp:tactical} *} |
13 chapter {* Tactical Reasoning\label{chp:tactical} *} |
14 |
14 |
1829 *} |
1829 *} |
1830 |
1830 |
1831 ML %linenosgray{*fun fail_simproc simpset redex = |
1831 ML %linenosgray{*fun fail_simproc simpset redex = |
1832 let |
1832 let |
1833 val ctxt = Simplifier.the_context simpset |
1833 val ctxt = Simplifier.the_context simpset |
1834 val _ = tracing ("The redex: " ^ (string_of_cterm ctxt redex)) |
1834 val _ = pwriteln (Pretty.block [Pretty.str "The redex: ", pretty_cterm ctxt redex]) |
1835 in |
1835 in |
1836 NONE |
1836 NONE |
1837 end*} |
1837 end*} |
1838 |
1838 |
1839 text {* |
1839 text {* |
1901 *} |
1901 *} |
1902 |
1902 |
1903 ML{*fun fail_simproc' simpset redex = |
1903 ML{*fun fail_simproc' simpset redex = |
1904 let |
1904 let |
1905 val ctxt = Simplifier.the_context simpset |
1905 val ctxt = Simplifier.the_context simpset |
1906 val _ = tracing ("The redex: " ^ (string_of_term ctxt redex)) |
1906 val _ = pwriteln (Pretty.block [Pretty.str "The redex:", pretty_term ctxt redex]) |
1907 in |
1907 in |
1908 NONE |
1908 NONE |
1909 end*} |
1909 end*} |
1910 |
1910 |
1911 text {* |
1911 text {* |
1912 Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm} |
1912 Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm} |
1913 (therefore we printing it out using the function @{ML string_of_term in Syntax}). |
1913 (therefore we printing it out using the function @{ML pretty_term in Pretty}). |
1914 We can turn this function into a proper simproc using the function |
1914 We can turn this function into a proper simproc using the function |
1915 @{ML Simplifier.simproc_i}: |
1915 @{ML Simplifier.simproc_i}: |
1916 *} |
1916 *} |
1917 |
1917 |
1918 |
1918 |