legacy/oldfan/ch_fan/fan_summary.hl

   1 (* Fan summary file created by thales Dec 7, 2009 *)
   2
   3 (* mark unfinished material *)
   4
   5 let NOT_FOUND  =
   6   let NOT_IN_SYSTEM = define `NOT_IN_SYSTEM = F` in
   7   let FALSE_ALL = prove(`NOT_IN_SYSTEM ==> x`,MESON_TAC[NOT_IN_SYSTEM]) in
   8   fun x -> INST [(x,`x:bool`)] FALSE_ALL ;;
   9
  10
  11 (* FAN DEFINED *)
  12
  13
  14 let CTVTAQA_t = `! V E E'. FANO(V,E) /\ (E' SUBSET E) ==> FANO(V,E')`;;
  15 let CTVTAQA = NOT_FOUND CTVTAQA_t ;;
  16
  17 XOHLED;;
  18
  19 (* remarks follow in text, formal proof? *)
  20
  21 AAUHTVE;; (* contains the essential content of the lemma *)
  22
  23 ULEKUUB;;  (* from chapter on trig. phrased in terms of hypermaps.  The lemma isn't exactly proved. *)
  24
  25
  26 VBTIKLP;;
  27
  28
  29 IBZWFFH;;
  30
  31 (* JGIYDLE;; not done *)