64 Sign.add_types_global |
64 Sign.add_types_global |
65 [(Binding.make ("fun", @{here}), 2, NoSyn), |
65 [(Binding.make ("fun", @{here}), 2, NoSyn), |
66 (Binding.make ("prop", @{here}), 0, NoSyn), |
66 (Binding.make ("prop", @{here}), 0, NoSyn), |
67 (Binding.make ("itself", @{here}), 1, NoSyn), |
67 (Binding.make ("itself", @{here}), 1, NoSyn), |
68 (Binding.make ("dummy", @{here}), 0, NoSyn)] |
68 (Binding.make ("dummy", @{here}), 0, NoSyn)] |
69 #> Theory.add_deps_global "fun" (Theory.DType ("fun", [typ "'a", typ "'b"])) [] |
69 #> Theory.add_deps_global "fun" ((Defs.Type, "fun"), [typ "'a", typ "'b"]) [] |
70 #> Theory.add_deps_global "prop" (Theory.DType ("prop", [])) [] |
70 #> Theory.add_deps_global "prop" ((Defs.Type, "prop"), []) [] |
71 #> Theory.add_deps_global "itself" (Theory.DType ("itself", [typ "'a"])) [] |
71 #> Theory.add_deps_global "itself" ((Defs.Type, "itself"), [typ "'a"]) [] |
72 #> Theory.add_deps_global "dummy" (Theory.DType ("dummy", [])) [] |
72 #> Theory.add_deps_global "dummy" ((Defs.Type, "dummy"), []) [] |
73 #> Sign.add_nonterminals_global |
73 #> Sign.add_nonterminals_global |
74 (map (fn name => Binding.make (name, @{here})) |
74 (map (fn name => Binding.make (name, @{here})) |
75 (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", |
75 (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", |
76 "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", |
76 "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", |
77 "any", "prop'", "num_const", "float_const", "num_position", |
77 "any", "prop'", "num_const", "float_const", "num_position", |
196 (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), |
196 (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), |
197 (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("!!", 0, 0)), |
197 (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("!!", 0, 0)), |
198 (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn), |
198 (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn), |
199 (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn), |
199 (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn), |
200 (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")] |
200 (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")] |
201 #> Theory.add_deps_global "Pure.eq" (Theory.DConst ("Pure.eq", typ "'a => 'a => prop")) [] |
201 #> Theory.add_deps_global "Pure.eq" ((Defs.Constant, "Pure.eq"), [typ "'a"]) [] |
202 #> Theory.add_deps_global "Pure.imp" (Theory.DConst ("Pure.imp", typ "prop => prop => prop")) [] |
202 #> Theory.add_deps_global "Pure.imp" ((Defs.Constant, "Pure.imp"), []) [] |
203 #> Theory.add_deps_global "Pure.all" (Theory.DConst ("Pure.all", typ "('a => prop) => prop")) [] |
203 #> Theory.add_deps_global "Pure.all" ((Defs.Constant, "Pure.all"), [typ "'a"]) [] |
204 #> Theory.add_deps_global "Pure.type" (Theory.DConst ("Pure.type", typ "'a itself")) [] |
204 #> Theory.add_deps_global "Pure.type" ((Defs.Constant, "Pure.type"), [typ "'a"]) [] |
205 #> Theory.add_deps_global "Pure.dummy_pattern" (Theory.DConst ("Pure.dummy_pattern", typ "'a")) [] |
205 #> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Constant, "Pure.dummy_pattern"), [typ "'a"]) [] |
206 #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation |
206 #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation |
207 #> Sign.parse_translation Syntax_Trans.pure_parse_translation |
207 #> Sign.parse_translation Syntax_Trans.pure_parse_translation |
208 #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation |
208 #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation |
209 #> Sign.add_consts |
209 #> Sign.add_consts |
210 [(qualify (Binding.make ("term", @{here})), typ "'a => prop", NoSyn), |
210 [(qualify (Binding.make ("term", @{here})), typ "'a => prop", NoSyn), |