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