equal
deleted
inserted
replaced
61 syntax (xsymbols) |
61 syntax (xsymbols) |
62 "_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) |
62 "_Pi" :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10) |
63 |
63 |
64 print_translation {* |
64 print_translation {* |
65 [(@{const_syntax Prod}, |
65 [(@{const_syntax Prod}, |
66 Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] |
66 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] |
67 *} |
67 *} |
68 |
68 |
69 axiomatization where |
69 axiomatization where |
70 s_b: "*: \<box>" and |
70 s_b: "*: \<box>" and |
71 |
71 |