equal
deleted
inserted
replaced
159 fun conn @{const_name True} = SOME "true" |
159 fun conn @{const_name True} = SOME "true" |
160 | conn @{const_name False} = SOME "false" |
160 | conn @{const_name False} = SOME "false" |
161 | conn @{const_name Not} = SOME "not" |
161 | conn @{const_name Not} = SOME "not" |
162 | conn @{const_name "op &"} = SOME "and" |
162 | conn @{const_name "op &"} = SOME "and" |
163 | conn @{const_name "op |"} = SOME "or" |
163 | conn @{const_name "op |"} = SOME "or" |
164 | conn @{const_name "op -->"} = SOME "implies" |
164 | conn @{const_name HOL.implies} = SOME "implies" |
165 | conn @{const_name "op ="} = SOME "iff" |
165 | conn @{const_name "op ="} = SOME "iff" |
166 | conn @{const_name If} = SOME "if_then_else" |
166 | conn @{const_name If} = SOME "if_then_else" |
167 | conn _ = NONE |
167 | conn _ = NONE |
168 |
168 |
169 fun pred @{const_name distinct} _ = SOME "distinct" |
169 fun pred @{const_name distinct} _ = SOME "distinct" |