README; bx branch

seeing what will happen when comitting to new bx branch
security predicates; forall assumptions

to avoid figuring out conflicts between (T w) and (p w) where p is
a user-defined predicate, hard-coding a bunch of SECPRED predicates
in the lexer and theory file.

the parser now accepts formulas    (forall (x) p)
desugaring now accepts             /*: p */ "#assume";
first batch of tests/djs/bx/ micro-examples

* removed SECPRED
- no longer need to hard-code the BX-related predicates in langLexer.mll
- BX predicates moved from theory.smt2 to bx/__bxpreds.smt2
  theory.smt2
- resolved parsing conflict between (T w) and (p ws) by requiring the former
  _not_ to be a type term. anyway, don't really want to write (U w) instead
  of (w :: U).

* #use from DJS
- can now load additional .dref files with   /*: "file.dref" */ "#use";
- entrypoint to parser in Main tweaked so that these #use directives
  get expanded even in DJS mode, not just !D mode

* js_threek
- changed type so that can call with arguments with different tags

* removed Settings.printShortQuick

* Sub.weakenArrowHeaps
- allow frzn weak locs to be added

* dsMethCall
- now using polyArgs only for the call, not the method retrieval itself
  (finally surfaced as an issue in simplemag00.js)
- if ever need to specify args for the getElem call, add a new kind of
  jsAppArgs annotation

* initial typing environment
- considering use of type vars like Url, Evt, Sty to model abstract types
  in APIs
sweet nested ref trick for getEltsByTagName!

gmail00 and newyork00 instantiate the guard to {FLS} and {TRU}
respectively to control whether the eltDoc predicate is included
FacePalm.f9 ported to face02.js
HoverMagnifier.f9 and Delicious.f9

* ported to hover02.js and delic01.js

* added [| T1, T2 |] tuple array syntax since <T1,T2> is ugly

* lazily adding not (undefined :: Ref m) predicates
- similar to not (null :: Ref l) from last month
- this change allows weak references to be stored in arrays Arr(NotUndef)

* Sub.dropNatives
- drops natives from arrow on _left_, assuming that natives aren't modified

* Sub.tempDropExistentialLocs
- allow locals to be dropped from arrow on _left_
- this is a fix until proper existential locations are implemented
JSTools.f9 and Untiny.f9
Typograf.f9
towards NitTwit.f9; first axioms in libraries
rest of NitTwit.f9
int loop examples; (-n) is sugar for (- 0 n)
more subtle loop examples; tweaking getPropArr

- added that a.length returns a (>= v 0) and that (>= (len theArr) 0)
- added if/then/else syntax in formulas
initArray examples
removing old parser/desugar/tc files
first few properties for wrapper nums/strings

  s.length
  s.charAt(0)
  n.toString()
remove djsDesugar.mli

missed this earlier. the files that were removed earlier were:
  langParser.mly
  djsDesugar.ml
  tcDref.ml*
  tcDref2.ml*
  tcUtils.ml*
adding Str case to types of <, <=, >, >=
Adding panos folder
Adding strobe folder
Type checked most of gadgets/morse.js. Added toLowerCase to fast path