IsabelleLight/make.ml

   1 (* ========================================================================= *)
   2 (*                              Isabelle Light                               *)
   3 (*   Isabelle/Procedural style additions and other user-friendly shortcuts.  *)
   4 (*                                                                           *)
   5 (*                   Petros Papapanagiotou, Jacques Fleuriot                 *)
   6 (*              Center of Intelligent Systems and their Applications         *)
   7 (*                          University of Edinburgh                          *)
   8 (*                                 2009-2012                                 *)
   9 (* ========================================================================= *)
  10 (* FILE         : make.ml                                                    *)
  11 (* DESCRIPTION  : Makefile. Simply calls the loader but it was written to    *)
  12 (*                match the rest of HOL Light's packages and for future use. *)
  13 (* LAST MODIFIED: October 2010                                               *)
  14 (* ========================================================================= *)
  15
  16 loads "IsabelleLight/isalight.ml";;
  17
  18 (* Some examples: *)
  19
  20 prove( `p/\q==>q`, rule impI THEN erule conjE THEN assumption);;
  21 prove (`(!x. P x) ==> P (y+1)`, rule impI THEN erule_tac [`a`,`y+1`] allE THEN assumption);;
  22 prove (`p\/q==>q\/p`, rule impI THEN erule disjE THENL [ rule disjI2 ; rule disjI1 ] THEN assumption);;
  23 prove (`p/\q ==> p\/q`, rule impI THEN rule disjI1 THEN drule conjunct1 THEN assumption);;
  24 prove (`p/\q ==> p\/q`, DISCH_TAC THEN DISJ1_TAC THEN FIRST_ASSUM(CONJUNCTS_THEN ACCEPT_TAC));;
  25 prove (`P x /\ x =0 ==> P 0`, rule impI THEN erule conjE THEN simp[]);;