https://github.com/JacquesCarette/hol-light
Revision 3041687a71afa02b00e52916f095010817bbc80d authored by aryafara on 21 June 2019, 20:59:16 UTC, committed by aryafara on 21 June 2019, 20:59:16 UTC
1 parent 9b01854
History
Tip revision: 3041687a71afa02b00e52916f095010817bbc80d authored by aryafara on 21 June 2019, 20:59:16 UTC
Manually went through list of both-modified files and replaced with hol-light\master variants, make should be usable now
Tip revision: 3041687
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