
;;; this is a comment

;; heuristics:

;; ### heuristic sets ###
;;   PL Heuristics + Struct. Ind.
;;   PL Heuristics + Case Splitting
;;   PL Heuristics
;;   Cntex Heuristics
;;   SC Heuristics
;;   DL Heuristics + Induction
;;   DL Heuristics + Case Splitting
;;   DL Heuristics
;;   DL Heuristics + Induction
;;   DL Heuristics + Case Splitting
;;   DL Heuristics
;;   TL Heuristics
;;   TL Heuristics + Exec
;; ### single heuristics
;;   module specific
;;   symbolic execution
;;   execute loop
;;   exec loop
;;   structural induction
;;   Replay
;;   induction
;;   simplifier
;;   weak simplifier
;;   strong simplifier
;;   elimination
;;   var elimination
;;   contract and execute
;;   unfold
;;   strong unfold
;;   weak unfold
;;   calls concrete
;;   calls nonrecursive
;;   calls flat
;;   bounded calls
;;   split
;;   conditional
;;   conditional right split
;;   conditional left split
;;   make lemma + continue
;;   batch mode
;;   cntex batch mode
;;   omega
;;   loop exit
;;   unwind
;;   if-then-else split
;;   pl case distinction
;;   dl case distinction
;;   cut
;;   constructor cut
;;   strong weakening
;;   rewrite
;;   give value
;;   weak cut
;;   axiom cut
;;   Quantifier closing
;;   Quantifier
;;   lemma closing
;;   apply ind once
;;   apply VD induction
;;   proof lemma
;;   apply ind
;;   apply ind closing
;;   ### heuristics for basic rotate rules (usebasicrotaterules? options) = T ###
;;   close axiom
;;   prop nonsplit rotate
;;   prop split rotate
;;   quant discard
;;   quant split
;;   quant inst
;;   ### heuristics for basicrules (usebasicrules? options) = T ###
;;   axiom
;;   prop simplification
;;   insert equation
;;   prop split
;;   smart basic case distinction
;;   discard quantifier
;;   ### misc special heuristics for testing, internal use etc. ###
;;   subproof
;;   proofscript
;;   wrong goal
;;   ### heuristics for 3tap (3tap-available) = T ###
;;   standard tap
;;   deep tap
;;   broad tap
;;   simple tap
;;   Spass
;;   ###  heuristics for TL ###
;;   tl simplify
;;   tl execute
;;   tl call
;;   tl apply induction
;;   tl trace induction
;;   tl step
;;   tl exist case
;;   tl case distinction
;;   isc initiate
;;   isc extract states
;;   isc execute call
;;   isc step
;;   sc drop
;;   sc initiate
;;   sc wf
;;   sc step
;;   sc tlstep
;;   uml sc step
;;   ### Java heuristics ###   
;;   simple java stuff
;;   after simplify java stuff
;;   always doit java stuff

options:
Replay: Use simprules of old proofsteps only
;;	use kodkod

;; simplifier:

;;       simp add <feature>
;;       simp delete <feature>
;;       forward add <feature>
;;       forward delete <feature>

configs:
;;    load libraries
;;    new spec names
;;    no exit all
;;    no work on library
;;    no proof locks for library
;;    hide library
;;    no directory locks
;;    ignore all errors
;;    update code

