Files

 master

/

meta-theory

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

hrutvik

Fix exp_eqSimps

May 10, 2025

f992888 · May 10, 2025

History

History

/

meta-theory

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
Holmakefile		Holmakefile	Reorganise all files	Dec 5, 2020
exp_eqSimps.sig		exp_eqSimps.sig	Give exp_eqSimps a signature	May 27, 2022
exp_eqSimps.sml		exp_eqSimps.sml	Fix exp_eqSimps	May 10, 2025
pure_alpha_equivScript.sml		pure_alpha_equivScript.sml	Fix for adjusted Inductive syntax in HOL	Nov 8, 2023
pure_barendregtScript.sml		pure_barendregtScript.sml	Fix a Barendregt cheat	Sep 19, 2023
pure_beta_equivScript.sml		pure_beta_equivScript.sml	Define Barendregt convention	Sep 4, 2023
pure_congruenceScript.sml		pure_congruenceScript.sml	Fix for adjusted Inductive syntax in HOL	Nov 8, 2023
pure_congruence_lemmasScript.sml		pure_congruence_lemmasScript.sml	Use exp_eq simplification to make some goals easier	May 27, 2022
pure_ctxt_equivScript.sml		pure_ctxt_equivScript.sml	Use HOL4's :itree rather than :io in misc	Mar 25, 2022
pure_demandScript.sml		pure_demandScript.sml	Fix for adjusted Inductive syntax in HOL	Nov 8, 2023
pure_eval_lemmasScript.sml		pure_eval_lemmasScript.sml	Fix gs usage in pure_eval_lemmas	Dec 6, 2021
pure_eval_surjScript.sml		pure_eval_surjScript.sml	Fix pure_eval_surj after change in HOL	Sep 9, 2024
pure_exp_lemmasScript.sml		pure_exp_lemmasScript.sml	Remove some duplicates	Oct 11, 2023
pure_exp_relScript.sml		pure_exp_relScript.sml	Fix pure_exp_relTheory	May 10, 2025
pure_inline_relScript.sml		pure_inline_relScript.sml	Fix for adjusted Inductive syntax in HOL	Nov 8, 2023
pure_letrec_congScript.sml		pure_letrec_congScript.sml	Complete a round of moves / clean up	Jun 20, 2023
pure_letrec_delargScript.sml		pure_letrec_delargScript.sml	Fix for adjusted Inductive syntax in HOL	Nov 8, 2023
pure_letrec_seqScript.sml		pure_letrec_seqScript.sml	Fix for adjusted Inductive syntax in HOL	Nov 8, 2023
pure_letrec_specScript.sml		pure_letrec_specScript.sml	Fix for adjusted Inductive syntax in HOL	Nov 8, 2023
pure_obs_sem_equalScript.sml		pure_obs_sem_equalScript.sml	Use HOL4's :itree rather than :io in misc	Mar 25, 2022
View all files