equal
deleted
inserted
replaced
45 "A * B" => "CONST Sigma(A, %_. B)" |
45 "A * B" => "CONST Sigma(A, %_. B)" |
46 "{x: A. B}" == "CONST Subtype(A, %x. B)" |
46 "{x: A. B}" == "CONST Subtype(A, %x. B)" |
47 |
47 |
48 print_translation {* |
48 print_translation {* |
49 [(@{const_syntax Pi}, |
49 [(@{const_syntax Pi}, |
50 Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), |
50 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), |
51 (@{const_syntax Sigma}, |
51 (@{const_syntax Sigma}, |
52 Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] |
52 fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] |
53 *} |
53 *} |
54 |
54 |
55 defs |
55 defs |
56 Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" |
56 Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" |
57 Unit_def: "Unit == {x. x=one}" |
57 Unit_def: "Unit == {x. x=one}" |