Commits

Show all
Author Commit Message Labels Comments Date
Paweł Wieczorek
Model.Valid: removed extensionality from Soundness theorem
Tags
coq_internal_error
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: Partial script for EQ_SBAPP
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: removed Beta rule from Soundness thoerem
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: removed SB_EXT rule from Model soundness theorem
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: removed SB rule from Soundness_theorem
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
minor
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: Beta-reduction, Extensionality
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: Helper for SB_EXT
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: Helper for SB
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Fixes in system.
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: a lot of rules with admits
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Syntax.System: a lot of fixes
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_CONG_SB
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: removed SB_F from theorem
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: SB_F as Helper
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: another helper EQ_TP_VALID
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_SB_SYM and EQ_SB_TRANS as helpers
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Syntax.System: fixes...
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_CONG_FUN_E
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: new tactics
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Syntax.System: fixed rule EQ_CONG_SB
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Syntax.System: fixed rule EQ_CONG_FUN_E
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_CONV_ABS
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_Valid
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_TP_Valid
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_TP_TRANS/SYM as helpers
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: added EQ_TP_SB_UNIT
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_TP_SB_NAT
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: EQ_TP_SSEQ
Branches
2011_11_16_model_soundness_theorem
Paweł Wieczorek
Model.Valid: added EQ_TP_CONG_SB
Branches
2011_11_16_model_soundness_theorem
  1. Prev
  2. Next