https://github.com/JacquesCarette/hol-light
History
Tip revision: b27a524086caf73530b7c2c5da1b237d3539f143 authored by Jacques Carette on 24 August 2020, 14:18:07 UTC
Merge pull request #35 from sjjs7/final-changes
Tip revision: b27a524
File Mode Size
Abstractions_and_quantifiers.ml -rw-r--r-- 820 bytes
Changing_proof_style.ml -rw-r--r-- 1.8 KB
Custom_inference_rules.ml -rw-r--r-- 5.9 KB
Custom_tactics.ml -rw-r--r-- 5.1 KB
Defining_new_types.ml -rw-r--r-- 4.5 KB
Embedding_of_logics_deep.ml -rw-r--r-- 4.3 KB
Embedding_of_logics_shallow.ml -rw-r--r-- 860 bytes
HOL_as_a_functional_programming_language.ml -rw-r--r-- 6.5 KB
HOL_basics.ml -rw-r--r-- 212 bytes
HOLs_number_systems.ml -rw-r--r-- 3.5 KB
Inductive_datatypes.ml -rw-r--r-- 2.7 KB
Inductive_definitions.ml -rw-r--r-- 3.8 KB
Linking_external_tools.ml -rw-r--r-- 5.5 KB
Number_theory.ml -rw-r--r-- 4.6 KB
Propositional_logic.ml -rw-r--r-- 753 bytes
Real_analysis.ml -rw-r--r-- 3.0 KB
Recursive_definitions.ml -rw-r--r-- 2.5 KB
Semantics_of_programming_languages_deep.ml -rw-r--r-- 3.5 KB
Semantics_of_programming_languages_shallow.ml -rw-r--r-- 8.5 KB
Sets_and_functions.ml -rw-r--r-- 1.9 KB
Tactics_and_tacticals.ml -rw-r--r-- 1.8 KB
Vectors.ml -rw-r--r-- 3.5 KB
Wellfounded_induction.ml -rw-r--r-- 577 bytes
all.ml -rw-r--r-- 81.4 KB

back to top