equal
deleted
inserted
replaced
45 |
45 |
46 text {* and undeclare the first one by: *} |
46 text {* and undeclare the first one by: *} |
47 |
47 |
48 declare rule1[foo del] |
48 declare rule1[foo del] |
49 |
49 |
50 text {* and query the remaining ones by: *} |
50 text {* and query the remaining ones with: |
51 |
51 |
52 thm foo |
52 @{ML_response_fake_both [display] "thm foo" |
|
53 "?C |
|
54 ?B"} |
53 |
55 |
54 text {* |
|
55 On the ML-level the rules marked with @{text "foo"} an be retrieved |
56 On the ML-level the rules marked with @{text "foo"} an be retrieved |
56 using the function @{ML FooRules.get}: |
57 using the function @{ML FooRules.get}: |
57 |
58 |
58 @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} |
59 @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} |
59 |
60 |
60 \begin{readmore} |
61 \begin{readmore} |
61 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
62 For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also |
|
63 the recipe in Section~\ref{recipe:storingdata} about storing arbitrary |
|
64 data. |
62 \end{readmore} |
65 \end{readmore} |
63 *} |
66 *} |
64 |
67 |
65 text {* |
68 text {* |
66 (FIXME: maybe add a comment about the case when the theorems |
69 (FIXME: maybe add a comment about the case when the theorems |