168 ("_context_xconst", typ "id_position => logic", Delimfix "XCONST _"), |
168 ("_context_xconst", typ "id_position => logic", Delimfix "XCONST _"), |
169 ("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"), |
169 ("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"), |
170 ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"), |
170 ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"), |
171 ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"), |
171 ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"), |
172 (const "==>", typ "prop => prop => prop", Delimfix "op ==>"), |
172 (const "==>", typ "prop => prop => prop", Delimfix "op ==>"), |
173 (const "dummy_pattern", typ "aprop", Delimfix "'_"), |
173 (const "Pure.dummy_pattern", typ "aprop", Delimfix "'_"), |
174 ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), |
174 ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), |
175 (const "Pure.term", typ "logic => prop", Delimfix "TERM _"), |
175 (const "Pure.term", typ "logic => prop", Delimfix "TERM _"), |
176 (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] |
176 (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] |
177 #> Sign.add_syntax Syntax.mode_default applC_syntax |
177 #> Sign.add_syntax Syntax.mode_default applC_syntax |
178 #> Sign.add_syntax (Symbol.xsymbolsN, true) |
178 #> Sign.add_syntax (Symbol.xsymbolsN, true) |
198 [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)), |
198 [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)), |
199 (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), |
199 (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), |
200 (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)), |
200 (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)), |
201 (Binding.name "prop", typ "prop => prop", NoSyn), |
201 (Binding.name "prop", typ "prop => prop", NoSyn), |
202 (Binding.name "TYPE", typ "'a itself", NoSyn), |
202 (Binding.name "TYPE", typ "'a itself", NoSyn), |
203 (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")] |
203 (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")] |
204 #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") [] |
204 #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") [] |
205 #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") [] |
205 #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") [] |
206 #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") [] |
206 #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") [] |
207 #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") [] |
207 #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") [] |
208 #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") [] |
208 #> Theory.add_deps_global "Pure.dummy_pattern" ("Pure.dummy_pattern", typ "'a") [] |
209 #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation |
209 #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation |
210 #> Sign.parse_translation Syntax_Trans.pure_parse_translation |
210 #> Sign.parse_translation Syntax_Trans.pure_parse_translation |
211 #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation |
211 #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation |
212 #> Sign.add_consts |
212 #> Sign.add_consts |
213 [(qualify (Binding.name "term"), typ "'a => prop", NoSyn), |
213 [(qualify (Binding.name "term"), typ "'a => prop", NoSyn), |