equal
deleted
inserted
replaced
390 |
390 |
391 (* ------------------------------------------------------------------------- *) |
391 (* ------------------------------------------------------------------------- *) |
392 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) |
392 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) |
393 (* ------------------------------------------------------------------------- *) |
393 (* ------------------------------------------------------------------------- *) |
394 |
394 |
395 val typ_of_dtyp = ATP_Util.typ_of_dtyp |
395 val typ_of_dtyp = Nitpick_Util.typ_of_dtyp |
396 |
396 |
397 (* ------------------------------------------------------------------------- *) |
397 (* ------------------------------------------------------------------------- *) |
398 (* close_form: universal closure over schematic variables in 't' *) |
398 (* close_form: universal closure over schematic variables in 't' *) |
399 (* ------------------------------------------------------------------------- *) |
399 (* ------------------------------------------------------------------------- *) |
400 |
400 |