Changeset 990 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 17, 2011, 1:30:01 PM (8 years ago)
Author:
sacerdot
Message:

Do no longer use the daemon automatically :-)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r985 r990  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
     4
     5(* let's implement a daemon not used by automation *)
     6inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX.
     7axiom IMPOSSIBLE: K1DAEMONXXX = K2DAEMONXXX.
     8example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
     9example not_implemented: False. cases daemon qed.
    410 
    511lemma eq_rect_Type0_r :
Note: See TracChangeset for help on using the changeset viewer.