equal
deleted
inserted
replaced
26 time_use_thy "Brouwer"; (*Infinite-branching trees*) |
26 time_use_thy "Brouwer"; (*Infinite-branching trees*) |
27 time_use_thy "Enum"; (*Enormous enumeration type*) |
27 time_use_thy "Enum"; (*Enormous enumeration type*) |
28 |
28 |
29 (** Inductive definitions **) |
29 (** Inductive definitions **) |
30 time_use_thy "Rmap"; (*mapping a relation over a list*) |
30 time_use_thy "Rmap"; (*mapping a relation over a list*) |
31 time_use_thy "Mutil"; (*mutilated checkerboard*) |
31 time_use_thy "Mutil"; (*mutilated chess board*) |
32 time_use_thy "PropLog"; (*completeness of propositional logic*) |
32 time_use_thy "PropLog"; (*completeness of propositional logic*) |
33 (*two Coq examples by Christine Paulin-Mohring*) |
33 (*two Coq examples by Christine Paulin-Mohring*) |
34 time_use_thy "ListN"; |
34 time_use_thy "ListN"; |
35 time_use_thy "Acc"; |
35 time_use_thy "Acc"; |
36 time_use_thy "Comb"; (*Combinatory Logic example*) |
36 time_use_thy "Comb"; (*Combinatory Logic example*) |