 |
|
|
|
.. (parent) |
 |
- |
rw-r--r-- |
820 |
Abstractions_and_quantifiers.ml
|
|
- |
rw-r--r-- |
1,851 |
Changing_proof_style.ml
|
|
- |
rw-r--r-- |
6,090 |
Custom_inference_rules.ml
|
|
- |
rw-r--r-- |
5,261 |
Custom_tactics.ml
|
|
- |
rw-r--r-- |
4,585 |
Defining_new_types.ml
|
|
- |
rw-r--r-- |
4,454 |
Embedding_of_logics_deep.ml
|
|
- |
rw-r--r-- |
860 |
Embedding_of_logics_shallow.ml
|
|
- |
rw-r--r-- |
6,671 |
HOL_as_a_functional_programming_language.ml
|
|
- |
rw-r--r-- |
212 |
HOL_basics.ml
|
|
- |
rw-r--r-- |
3,562 |
HOLs_number_systems.ml
|
|
- |
rw-r--r-- |
2,728 |
Inductive_datatypes.ml
|
|
- |
rw-r--r-- |
3,932 |
Inductive_definitions.ml
|
|
- |
rw-r--r-- |
5,650 |
Linking_external_tools.ml
|
|
- |
rw-r--r-- |
4,668 |
Number_theory.ml
|
|
- |
rw-r--r-- |
753 |
Propositional_logic.ml
|
|
- |
rw-r--r-- |
3,062 |
Real_analysis.ml
|
|
- |
rw-r--r-- |
2,598 |
Recursive_definitions.ml
|
|
- |
rw-r--r-- |
3,549 |
Semantics_of_programming_languages_deep.ml
|
|
- |
rw-r--r-- |
8,704 |
Semantics_of_programming_languages_shallow.ml
|
|
- |
rw-r--r-- |
1,978 |
Sets_and_functions.ml
|
|
- |
rw-r--r-- |
1,845 |
Tactics_and_tacticals.ml
|
|
- |
rw-r--r-- |
3,579 |
Vectors.ml
|
|
- |
rw-r--r-- |
577 |
Wellfounded_induction.ml
|
|
- |
rw-r--r-- |
83,353 |
all.ml
|
