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,gray] "thm foo" |
51 \begin{isabelle} |
52 "?C |
52 \isacommand{thm}~@{text "foo"}\\ |
53 ?B"} |
53 @{text "> ?C"}\\ |
|
54 @{text "> ?B"}\\ |
|
55 \end{isabelle} |
54 |
56 |
55 On the ML-level the rules marked with @{text "foo"} an be retrieved |
57 On the ML-level the rules marked with @{text "foo"} an be retrieved |
56 using the function @{ML FooRules.get}: |
58 using the function @{ML FooRules.get}: |
57 |
59 |
58 @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} |
60 @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} |