Commit 94b2c162 authored by Magnus Myreen's avatar Magnus Myreen

Attempt to fix problem with preamble

parent 61519f34
......@@ -3,11 +3,8 @@
development.
*)
open HolKernel bossLib boolLib boolSimps lcsymtacs Parse
open optionTheory combinTheory listTheory pred_setTheory
finite_mapTheory alistTheory rich_listTheory llistTheory
arithmeticTheory pairTheory sortingTheory relationTheory
totoTheory comparisonTheory bitTheory sptreeTheory wordsTheory
set_sepTheory indexedListsTheory ASCIInumbersLib
open optionTheory combinTheory listTheory pred_setTheory finite_mapTheory alistTheory rich_listTheory llistTheory arithmeticTheory pairTheory sortingTheory relationTheory totoTheory comparisonTheory bitTheory sptreeTheory wordsTheory set_sepTheory indexedListsTheory
ASCIInumbersLib
(* Misc. lemmas (without any compiler constants) *)
val _ = new_theory "misc"
......
......@@ -188,7 +188,13 @@ fun any_match_mp impth th =
in
MATCH_MP th2 th end
val SWAP_IMP = PROVE[]``(P ==> Q ==> R) ==> (Q ==> P ==> R)``
val SWAP_IMP = let
val P = mk_var("P", bool)
val Q = mk_var("Q", bool)
val R = mk_var("R", bool)
in
PROVE[] (mk_imp(list_mk_imp([P,Q], R), list_mk_imp([Q,P], R)))
end
fun prove_hyps_by tac th = foldr (uncurry PROVE_HYP) th (map (fn h => prove(h,tac)) (hyp th));
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment