equal
deleted
inserted
replaced
412 |
412 |
413 end; |
413 end; |
414 |
414 |
415 val op aconvc = Thm.aconvc; |
415 val op aconvc = Thm.aconvc; |
416 |
416 |
417 structure Thmtab = TableFun(type key = thm val ord = Thm.thm_ord); |
417 structure Thmtab = Table(type key = thm val ord = Thm.thm_ord); |