1signature Sanity = 2sig 3 4 type term = Term.term 5 type thm = Thm.thm 6 type theory = Hol_pp.theory 7 type tactic = Abbrev.tactic 8 9 val accepted_axioms : string list ref; 10 val accepted_oracles : string list ref; 11 12 (* Traces 13 14 "Santity Check Strict": 15 ------------------------ 16 Turn warnings or exception on or off. 17 Default: true (through exception) 18 19 "Santity Check Verbose": 20 ------------------------ 21 Turn verbose reporting on or off. 22 Default: true 23 24 25 "Santity Check Free Vars": 26 -------------------------- 27 Turn checking for free top-level variables to different levels: 28 0 : allow no free vars 29 1 : if theorem starts with an allquantor, then allow no free vars 30 2 : no check 31 Default: 1 32 33 34 "Santity Check Var-Const Clash": 35 -------------------------------- 36 Turn checks whether constant names are used as variables on or off. 37 Default: true 38 39 40 "Santity Check Thm-Name Clash": 41 ------------------------------- 42 Turn checks whether the same theorem name is used in multiple theories. 43 Default: true 44 45 *) 46 47 48 (* sanity checks the given theory *) 49 val sanity_check_theory : string -> bool 50 51 (* sanity checks the current theory *) 52 val sanity_check : unit -> bool 53 54 (* sanity checks all loaded theories *) 55 val sanity_check_all : unit -> bool 56 57 (* sanity checks a theorem *) 58 val sanity_check_thm : thm -> bool 59 60 (* sanity checks a theorem with a given name *) 61 val sanity_check_named_thm : (string * thm) -> bool 62 63 64 (* versions of prove, store_thm and save_thm that perform checks, 65 see trace "Sanity Check Strict" *) 66 val sanity_prove : (term * tactic) -> thm 67 val save_thm : (string * thm) -> thm 68 val store_thm : (string * term * tactic) -> thm 69 70end 71