Skip to content
Navigation Menu
Sign in
Appearance settings
Platform
AI CODE CREATION
GitHub Copilot
Write better code with AI
GitHub Copilot app
Direct agents from issue to merge
MCP Registry
Integrate external tools
DEVELOPER WORKFLOWS
Actions
Automate any workflow
Codespaces
Instant dev environments
Issues
Plan and track work
Code Review
Manage code changes
Code Quality
Enforce quality at merge
APPLICATION SECURITY
GitHub Advanced Security
Find and fix vulnerabilities
Code security
Secure your code as you build
Secret protection
Stop leaks before they start
EXPLORE
Why GitHub
Documentation
Blog
Changelog
Marketplace
View all features
Solutions
BY COMPANY SIZE
Enterprises
Small and medium teams
Startups
Nonprofits
BY USE CASE
App Modernization
DevSecOps
DevOps
CI/CD
View all use cases
BY INDUSTRY
Healthcare
Financial services
Manufacturing
Government
View all industries
View all solutions
Resources
EXPLORE BY TOPIC
AI
Software Development
DevOps
Security
View all topics
EXPLORE BY TYPE
Customer stories
Events & webinars
Ebooks & reports
Business insights
GitHub Skills
SUPPORT & SERVICES
Documentation
Customer support
Community forum
Trust center
Partners
View all resources
Open Source
COMMUNITY
GitHub Sponsors
Fund open source developers
PROGRAMS
Security Lab
Maintainer Community
GitHub Stars
Archive Program
REPOSITORIES
Topics
Trending
Collections
Enterprise
ENTERPRISE SOLUTIONS
Enterprise platform
AI-powered developer platform
AVAILABLE ADD-ONS
GitHub Advanced Security
Enterprise-grade security features
Copilot for Business
Enterprise-grade AI features
Premium Support
Enterprise-grade 24/7 support
Pricing
Search
/
Sign in
Sign up
Appearance settings
You signed in with another tab or window.
Reload
to refresh your session.
You signed out in another tab or window.
Reload
to refresh your session.
You switched accounts on another tab or window.
Reload
to refresh your session.
Dismiss alert
{{ message }}
linhua55
/
hol-light
Public
forked from
jrh13/hol-light
Notifications
You must be signed in to change notification settings
Fork
0
Star
0
Code
Pull requests
0
Actions
Projects
Security and quality
0
Insights
Additional navigation options
Code
Pull requests
Actions
Projects
Security and quality
Insights
Files
Expand file tree
master
Breadcrumbs
hol-light
/
Help
/
Copy path
Directory actions
More options
More options
Directory actions
More options
More options
Latest commit
History
History
History
master
Breadcrumbs
hol-light
/
Help
/
Copy path
Top
Folders and files
Name
Name
Last commit message
Last commit date
parent directory
..
.joinparsers.doc
.joinparsers.doc
.orparser.doc
.orparser.doc
.pipeparser.doc
.pipeparser.doc
.singlefun.doc
.singlefun.doc
.upto.doc
.upto.doc
.valmod.doc
.valmod.doc
ABBREV_TAC.doc
ABBREV_TAC.doc
ABS.doc
ABS.doc
ABS_CONV.doc
ABS_CONV.doc
ABS_TAC.doc
ABS_TAC.doc
AC.doc
AC.doc
ACCEPT_TAC.doc
ACCEPT_TAC.doc
ADD_ASSUM.doc
ADD_ASSUM.doc
ALL_CONV.doc
ALL_CONV.doc
ALL_TAC.doc
ALL_TAC.doc
ALL_THEN.doc
ALL_THEN.doc
ALPHA_CONV.doc
ALPHA_CONV.doc
ALPHA_UPPERCASE.doc
ALPHA_UPPERCASE.doc
ANTE_RES_THEN.doc
ANTE_RES_THEN.doc
ANTS_TAC.doc
ANTS_TAC.doc
AP_TERM.doc
AP_TERM.doc
AP_TERM_TAC.doc
AP_TERM_TAC.doc
AP_THM.doc
AP_THM.doc
AP_THM_TAC.doc
AP_THM_TAC.doc
ARITH_RULE.doc
ARITH_RULE.doc
ARITH_TAC.doc
ARITH_TAC.doc
ASM.doc
ASM.doc
ASM_ARITH_TAC.doc
ASM_ARITH_TAC.doc
ASM_CASES_TAC.doc
ASM_CASES_TAC.doc
ASM_FOL_TAC.doc
ASM_FOL_TAC.doc
ASM_INT_ARITH_TAC.doc
ASM_INT_ARITH_TAC.doc
ASM_MESON_TAC.doc
ASM_MESON_TAC.doc
ASM_METIS_TAC.doc
ASM_METIS_TAC.doc
ASM_REAL_ARITH_TAC.doc
ASM_REAL_ARITH_TAC.doc
ASM_REWRITE_RULE.doc
ASM_REWRITE_RULE.doc
ASM_REWRITE_TAC.doc
ASM_REWRITE_TAC.doc
ASM_SIMP_TAC.doc
ASM_SIMP_TAC.doc
ASSOC_CONV.doc
ASSOC_CONV.doc
ASSUME.doc
ASSUME.doc
ASSUME_TAC.doc
ASSUME_TAC.doc
ASSUM_LIST.doc
ASSUM_LIST.doc
AUGMENT_SIMPSET.doc
AUGMENT_SIMPSET.doc
BETA.doc
BETA.doc
BETAS_CONV.doc
BETAS_CONV.doc
BETA_CONV.doc
BETA_CONV.doc
BETA_RULE.doc
BETA_RULE.doc
BETA_TAC.doc
BETA_TAC.doc
BINDER_CONV.doc
BINDER_CONV.doc
BINOP_CONV.doc
BINOP_CONV.doc
BINOP_TAC.doc
BINOP_TAC.doc
BOOL_CASES_TAC.doc
BOOL_CASES_TAC.doc
C.doc
C.doc
CACHE_CONV.doc
CACHE_CONV.doc
CASE_REWRITE_TAC.doc
CASE_REWRITE_TAC.doc
CCONTR.doc
CCONTR.doc
CHANGED_CONV.doc
CHANGED_CONV.doc
CHANGED_TAC.doc
CHANGED_TAC.doc
CHAR_EQ_CONV.doc
CHAR_EQ_CONV.doc
CHEAT_TAC.doc
CHEAT_TAC.doc
CHOOSE_TAC.doc
CHOOSE_TAC.doc
CHOOSE_THEN.doc
CHOOSE_THEN.doc
CHOOSE_UPPERCASE.doc
CHOOSE_UPPERCASE.doc
CLAIM_TAC.doc
CLAIM_TAC.doc
CNF_CONV.doc
CNF_CONV.doc
COMB2_CONV.doc
COMB2_CONV.doc
COMB_CONV.doc
COMB_CONV.doc
CONDS_CELIM_CONV.doc
CONDS_CELIM_CONV.doc
CONDS_ELIM_CONV.doc
CONDS_ELIM_CONV.doc
COND_CASES_TAC.doc
COND_CASES_TAC.doc
COND_ELIM_CONV.doc
COND_ELIM_CONV.doc
CONJ.doc
CONJ.doc
CONJUNCT1.doc
CONJUNCT1.doc
CONJUNCT2.doc
CONJUNCT2.doc
CONJUNCTS_THEN.doc
CONJUNCTS_THEN.doc
CONJUNCTS_THEN2.doc
CONJUNCTS_THEN2.doc
CONJUNCTS_UPPERCASE.doc
CONJUNCTS_UPPERCASE.doc
CONJ_ACI_RULE.doc
CONJ_ACI_RULE.doc
CONJ_CANON_CONV.doc
CONJ_CANON_CONV.doc
CONJ_PAIR.doc
CONJ_PAIR.doc
CONJ_TAC.doc
CONJ_TAC.doc
CONTR.doc
CONTR.doc
CONTRAPOS_CONV.doc
CONTRAPOS_CONV.doc
CONTR_TAC.doc
CONTR_TAC.doc
CONV_RULE.doc
CONV_RULE.doc
CONV_TAC.doc
CONV_TAC.doc
DEDUCT_ANTISYM_RULE.doc
DEDUCT_ANTISYM_RULE.doc
DENUMERAL.doc
DENUMERAL.doc
DEPTH_BINOP_CONV.doc
DEPTH_BINOP_CONV.doc
DEPTH_CONV.doc
DEPTH_CONV.doc
DEPTH_SQCONV.doc
DEPTH_SQCONV.doc
DESTRUCT_TAC.doc
DESTRUCT_TAC.doc
DISCH.doc
DISCH.doc
DISCH_ALL.doc
DISCH_ALL.doc
DISCH_TAC.doc
DISCH_TAC.doc
DISCH_THEN.doc
DISCH_THEN.doc
DISJ1.doc
DISJ1.doc
DISJ1_TAC.doc
DISJ1_TAC.doc
DISJ2.doc
DISJ2.doc
DISJ2_TAC.doc
DISJ2_TAC.doc
DISJ_ACI_RULE.doc
DISJ_ACI_RULE.doc
View all files
You can’t perform that action at this time.