26 |
26 |
27 fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); |
27 fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); |
28 fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range); |
28 fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range); |
29 fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range); |
29 fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range); |
30 fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range); |
30 fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range); |
31 |
|
32 fun add_deps_type c thy = |
|
33 let |
|
34 val n = Sign.arity_number thy c; |
|
35 val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); |
|
36 in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end |
|
37 |
|
38 fun add_deps_const c thy = |
|
39 let |
|
40 val T = Logic.unvarifyT_global (Sign.the_const_type thy c); |
|
41 val typargs = Sign.const_typargs thy (c, T); |
|
42 in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end; |
|
43 |
31 |
44 |
32 |
45 (* application syntax variants *) |
33 (* application syntax variants *) |
46 |
34 |
47 val appl_syntax = |
35 val appl_syntax = |
84 [(Binding.make ("fun", \<^here>), 2, NoSyn), |
72 [(Binding.make ("fun", \<^here>), 2, NoSyn), |
85 (Binding.make ("prop", \<^here>), 0, NoSyn), |
73 (Binding.make ("prop", \<^here>), 0, NoSyn), |
86 (Binding.make ("itself", \<^here>), 1, NoSyn), |
74 (Binding.make ("itself", \<^here>), 1, NoSyn), |
87 (Binding.make ("dummy", \<^here>), 0, NoSyn), |
75 (Binding.make ("dummy", \<^here>), 0, NoSyn), |
88 (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)] |
76 (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)] |
89 #> add_deps_type "fun" |
77 #> Theory.add_deps_type "fun" |
90 #> add_deps_type "prop" |
78 #> Theory.add_deps_type "prop" |
91 #> add_deps_type "itself" |
79 #> Theory.add_deps_type "itself" |
92 #> add_deps_type "dummy" |
80 #> Theory.add_deps_type "dummy" |
93 #> add_deps_type "Pure.proof" |
81 #> Theory.add_deps_type "Pure.proof" |
94 #> Sign.add_nonterminals_global |
82 #> Sign.add_nonterminals_global |
95 (map (fn name => Binding.make (name, \<^here>)) |
83 (map (fn name => Binding.make (name, \<^here>)) |
96 (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", |
84 (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", |
97 "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", |
85 "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", |
98 "any", "prop'", "num_const", "float_const", "num_position", |
86 "any", "prop'", "num_const", "float_const", "num_position", |
223 (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn), |
211 (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn), |
224 (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), |
212 (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), |
225 (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), |
213 (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn), |
226 (qualify (Binding.make ("PClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn), |
214 (qualify (Binding.make ("PClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn), |
227 (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)] |
215 (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)] |
228 #> add_deps_const "Pure.eq" |
216 #> Theory.add_deps_const "Pure.eq" |
229 #> add_deps_const "Pure.imp" |
217 #> Theory.add_deps_const "Pure.imp" |
230 #> add_deps_const "Pure.all" |
218 #> Theory.add_deps_const "Pure.all" |
231 #> add_deps_const "Pure.type" |
219 #> Theory.add_deps_const "Pure.type" |
232 #> add_deps_const "Pure.dummy_pattern" |
220 #> Theory.add_deps_const "Pure.dummy_pattern" |
233 #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation |
221 #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation |
234 #> Sign.parse_translation Syntax_Trans.pure_parse_translation |
222 #> Sign.parse_translation Syntax_Trans.pure_parse_translation |
235 #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation |
223 #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation |
236 #> Sign.add_consts |
224 #> Sign.add_consts |
237 [(qualify (Binding.make ("term", \<^here>)), typ "'a \<Rightarrow> prop", NoSyn), |
225 [(qualify (Binding.make ("term", \<^here>)), typ "'a \<Rightarrow> prop", NoSyn), |