equal
deleted
inserted
replaced
48 print_translation {* |
48 print_translation {* |
49 [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), |
49 [(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), |
50 (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] |
50 (@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] |
51 *} |
51 *} |
52 |
52 |
53 axioms |
53 defs |
54 Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" |
54 Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" |
55 Unit_def: "Unit == {x. x=one}" |
55 Unit_def: "Unit == {x. x=one}" |
56 Bool_def: "Bool == {x. x=true | x=false}" |
56 Bool_def: "Bool == {x. x=true | x=false}" |
57 Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" |
57 Plus_def: "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}" |
58 Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" |
58 Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" |