2640

1 

15649

2 
(* legacy ML bindings *)

2640

3 

15649

4 
val TT_def = thm "TT_def";


5 
val FF_def = thm "FF_def";


6 
val neg_def = thm "neg_def";


7 
val ifte_def = thm "ifte_def";


8 
val andalso_def = thm "andalso_def";


9 
val orelse_def = thm "orelse_def";


10 
val If2_def = thm "If2_def";


11 
val Exh_tr = thm "Exh_tr";


12 
val trE = thm "trE";


13 
val tr_defs = thms "tr_defs";


14 
val dist_less_tr = thms "dist_less_tr";


15 
val dist_eq_tr = thms "dist_eq_tr";


16 
val ifte_simp = thm "ifte_simp";


17 
val ifte_thms = thms "ifte_thms";


18 
val andalso_thms = thms "andalso_thms";


19 
val orelse_thms = thms "orelse_thms";


20 
val neg_thms = thms "neg_thms";


21 
val split_If2 = thm "split_If2";


22 
val andalso_or = thm "andalso_or";


23 
val andalso_and = thm "andalso_and";


24 
val Def_bool1 = thm "Def_bool1";


25 
val Def_bool2 = thm "Def_bool2";


26 
val Def_bool3 = thm "Def_bool3";


27 
val Def_bool4 = thm "Def_bool4";


28 
val If_and_if = thm "If_and_if";


29 
val adm_trick_1 = thm "adm_trick_1";


30 
val adm_trick_2 = thm "adm_trick_2";


31 
val adm_tricks = thms "adm_tricks";


32 
val adm_nTT = thm "adm_nTT";


33 
val adm_nFF = thm "adm_nFF";

2640

34 
