| changeset 227 | a00c7721fc3b |
| parent 222 | 1dc03eaa7cb9 |
| parent 226 | 98f53ab3722e |
| child 228 | fe45fbb111c5 |
| 225:7859fc59249a | 227:a00c7721fc3b |
|---|---|
924 in |
924 in |
925 OuterSyntax.local_theory "foobar" "traces a proposition" |
925 OuterSyntax.local_theory "foobar" "traces a proposition" |
926 kind trace_prop_parser |
926 kind trace_prop_parser |
927 end *} |
927 end *} |
928 |
928 |
929 |
|
929 text {* |
930 text {* |
930 Now you can type |
931 Now you can type |
931 |
932 |
932 \begin{isabelle} |
933 \begin{isabelle} |
933 \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\ |
934 \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\ |