equal
deleted
inserted
replaced
55 Let us start with the translation function from Isabelle propositions into |
55 Let us start with the translation function from Isabelle propositions into |
56 the solver's string representation. To increase efficiency while building |
56 the solver's string representation. To increase efficiency while building |
57 the string, we use functions from the @{text Buffer} module. |
57 the string, we use functions from the @{text Buffer} module. |
58 *} |
58 *} |
59 |
59 |
60 ML {*fun translate t = |
60 ML %grayML{*fun translate t = |
61 let |
61 let |
62 fun trans t = |
62 fun trans t = |
63 (case t of |
63 (case t of |
64 @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u => |
64 @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u => |
65 Buffer.add " (" #> |
65 Buffer.add " (" #> |
70 | Free (n, @{typ bool}) => |
70 | Free (n, @{typ bool}) => |
71 Buffer.add " " #> |
71 Buffer.add " " #> |
72 Buffer.add n #> |
72 Buffer.add n #> |
73 Buffer.add " " |
73 Buffer.add " " |
74 | _ => error "inacceptable term") |
74 | _ => error "inacceptable term") |
75 in Buffer.content (trans t Buffer.empty) end |
75 in Buffer.content (trans t Buffer.empty) end*} |
76 *} |
|
77 |
76 |
78 text {* |
77 text {* |
79 Here is the string representation of the term @{term "p = (q = p)"}: |
78 Here is the string representation of the term @{term "p = (q = p)"}: |
80 |
79 |
81 @{ML_response |
80 @{ML_response |