equal
deleted
inserted
replaced
361 |
361 |
362 datatype thm = Thm of |
362 datatype thm = Thm of |
363 {sign: Sign.sg, (*signature for hyps and prop*) |
363 {sign: Sign.sg, (*signature for hyps and prop*) |
364 der: deriv, (*derivation*) |
364 der: deriv, (*derivation*) |
365 maxidx: int, (*maximum index of any Var or TVar*) |
365 maxidx: int, (*maximum index of any Var or TVar*) |
366 shyps: sort list, (* FIXME comment *) |
366 shyps: sort list, (*sort hypotheses*) |
367 hyps: term list, (*hypotheses*) |
367 hyps: term list, (*hypotheses*) |
368 prop: term}; (*conclusion*) |
368 prop: term}; (*conclusion*) |
369 |
369 |
370 fun rep_thm (Thm args) = args; |
370 fun rep_thm (Thm args) = args; |
371 |
371 |