187 #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") [] |
187 #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") [] |
188 #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") [] |
188 #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") [] |
189 #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") [] |
189 #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") [] |
190 #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") [] |
190 #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") [] |
191 #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") [] |
191 #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") [] |
192 #> Sign.add_trfuns Syntax_Trans.pure_trfuns |
192 #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation |
|
193 #> Sign.parse_translation Syntax_Trans.pure_parse_translation |
|
194 #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation |
193 #> Sign.local_path |
195 #> Sign.local_path |
194 #> Sign.add_consts_i |
196 #> Sign.add_consts_i |
195 [(Binding.name "term", typ "'a => prop", NoSyn), |
197 [(Binding.name "term", typ "'a => prop", NoSyn), |
196 (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn), |
198 (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn), |
197 (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)] |
199 (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)] |