Skip to content

Commit

Permalink
Fix a theorem-naming nit in sorting
Browse files Browse the repository at this point in the history
ML-binding didn't match exported name
  • Loading branch information
mn200 committed Jul 28, 2016
1 parent 3633108 commit 4a1a542
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/sort/sortingScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -534,7 +534,7 @@ val QSORT_IND = fetch "-" "QSORT_IND";
* Properties of QSORT *
*---------------------------------------------------------------------------*)

val QSORT_MEM_STABLE = Q.store_thm
val QSORT_MEM = Q.store_thm
("QSORT_MEM",
`!R L x. MEM x (QSORT R L) = MEM x L`,
recInduct QSORT_IND
Expand Down Expand Up @@ -576,7 +576,7 @@ Q.store_thm
THEN MATCH_MP_TAC SORTED_APPEND
THEN POP_ASSUM (ASSUME_TAC o SYM)
THEN IMP_RES_THEN (fn th => ASM_REWRITE_TAC [th]) SORTED_EQ
THEN RW_TAC list_ss [MEM_FILTER,MEM,QSORT_MEM_STABLE]
THEN RW_TAC list_ss [MEM_FILTER,MEM,QSORT_MEM]
THEN ((RES_TAC THEN NO_TAC) ORELSE ALL_TAC)
THEN Q.PAT_ASSUM `x = y` (MP_TAC o MATCH_MP
(REWRITE_RULE[PROVE [] (Term `x/\y/\z ==> w = x ==> y/\z ==> w`)]
Expand Down

0 comments on commit 4a1a542

Please sign in to comment.