174 (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] |
174 (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] |
175 #> Sign.add_syntax Syntax.mode_default applC_syntax |
175 #> Sign.add_syntax Syntax.mode_default applC_syntax |
176 #> Sign.add_syntax (Symbol.xsymbolsN, true) |
176 #> Sign.add_syntax (Symbol.xsymbolsN, true) |
177 [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)), |
177 [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)), |
178 ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)), |
178 ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)), |
179 ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)), |
|
180 ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)), |
|
181 ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)), |
|
182 ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)), |
|
183 ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)), |
|
184 ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)), |
179 ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)), |
185 (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\<equiv>", 2)), |
180 (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\<equiv>", 2)), |
186 (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)), |
181 (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)), |
187 (const "Pure.imp", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)), |
182 (const "Pure.imp", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)), |
188 ("_DDDOT", typ "aprop", Delimfix "\\<dots>"), |
183 ("_DDDOT", typ "aprop", Delimfix "\\<dots>"), |