1+ ===================================================================== + 2| | 3| LIBRARY : meson | 4| | 5| DESCRIPTION : MESON Model Elimination first order theorem prover. | 6| | 7| AUTHOR : J.R.Harrison | 8| DATE : 1996 | 9| | 10| PORTED BY : D.R.Syme | 11| DATE : 1996 | 12| | 13| MODIFIED : R.J.Boulton | 14| DATE : 6 August 1996 | 15+ ===================================================================== + 16 17Relevant structures: Meson 18 19Functions: 20 val MESON : mset list -> thm list -> term -> thm 21 val MESON_TAC : mset list -> thm list -> tactic 22 val mk_mset : thm list -> mset 23 24