(*DOC*)theory iI(*DOC*)
imports Main
begin

section{* Jv Favorites *}
(*                     
--"INFO BEGIN=================================================================="
  --{*notation Trueprop("Tr")    notation "prop"("Pr")*}
  declare[[show_brackets=true]]  declare[[show_sorts=false]]
  declare[[names_long=false]]    declare[[show_types=true]]
  declare[[names_unique=true]]   declare[[show_consts=true]]
--"INFO END--------------------------------------------------------------------"
theorem show_info:
 "(True) =
  (True)"
  by(auto) 
  thm show_info
*)

section{* Misc Help Commands *}
(*help*)                         (*Lists the available commands.*)
help

section{* Show *}
declare[[show_brackets=true]] (*sub-exprs will be parenthesized*)
declare[[show_sorts=false]]   (*show type & sort constraints for term vars*)
declare[[show_types=true]]    (*show type constraints for term vars*)
declare[[names_long=false]]    (*names_long, names_short*)
declare[[names_unique=true]]  (*names_unique*)
declare[[show_consts=true]]   (*show constants when displaying a goal state*)

declare[[show_main_goal=true]](*main result to be proven is displayed*)
declare[[show_abbrevs=true]]  (*controls folding of constant abbreviations*)
declare[[eta_contract=false]] (*Isa performs eta-contractions before printing*)
declare[[goals_limit=100]]    (*max subgoals to be shown*)
declare[[show_hyps=true]]     (*show implicit hypotheses of local facts*)
declare[[show_tags=true]]     (*extra annotations within theorems*)
declare[[show_question_marks=true]](*question marks for schematic vars*)

(*From ~~/NEWS
syntax_ast_trace
syntax_ast_stat
syntax_ambiguity_level

rule_trace

thy_output_display
thy_output_quotes
thy_output_indent
thy_output_source
thy_output_break
*)

section{* Notation Tricks To Show Hidden Trueprop and prop *}
(*notation Trueprop  ("Tr")*)    (*Will display the hidden Trueprop function globally.*)
(*notation "prop" ("Pr")*)       (*Will  display the hidden prop function globally.*)
(*write Trueprop  ("Tr")*)       (*Use like "notation", but in notepad.*)

section{* Print Modes *}
(*isabelle jedit -m brackets     Start jEdit with print mode set to brackets*)
  (*
  brackets,                      Doesn't convert [|A;B|] ==> C|] in the goals.
  no_brackets,
  type_brackets,                 Control output of nested => (types)
  no_type_brackets
  iff                            Shows boolean equality as a double arrow.
  *)
(*ISABELLE_JEDIT_OPTIONS         In etc/settings gives default command line options.*)
(*ML{*print_mode_value();*}      List of currently active print mode names.*)


section{* Inspecting The Current Context *}
(*print_abbrevs     prints all constant abbreviations of the current context*)
(*print_attributes  all attributes available in the current theory context*)
(*print_binds       term abbreviations present in the context*)
(*print_bundles     prints the named bundles that are available in the current context*)
(*print_cases       prints all local contexts of the current state*)
(*print_claset      prints the collection of rules declared to the Classical Reasoner*)
(*print_classes     prints all classes in the current theory.*)
(*print_commands    outer theory syntax, including keywords and command*)
(*print_configs     prints available config options, with names, types, and current values*)
(*print_dependencies <expr> lists all locale instances for which interpretations would be added to the current context*)
(*print_facts       local facts of the current context, both named and unnamed*)
(*print_induct_rules      prints cases and induct rules for predicates (or sets) and types*)
(*print_interps <locale>  lists all interpretations of locale in the current theory or proof context*)
(*print_locale <locale>   prints the contents of the named locale; use ! to include notes*)
(*print_locales     prints the names of all locales of the current theory*)
(*print_methods     all proof methods available in the current theory context*)
(*print_simpset     prints the collection of rules declared to the Simplifier*)
(*print_statement <a> prints facts from the current theory or proof context in long statement form*)
(*print_syntax      prints the inner syntax of the current context*)
(*print_theorems !  theorems resulting from the last command; ! for verbosity*)
(*print_theory !    main logical content of theory context; ! for verbosity*)

section{* Find Commands *}
(*find_theorems <criteria>   facts from the theory or proof context matching criteria*)
(*find_consts <criteria>     all constants whose type meets all of the given criteria
  Example: find_consts  name: listT.Cons*)
(*thm_deps <a1...an>; visualizes dependencies of facts, using Isabelle's graph browser tool*)
(*unused_thms <A1...Am - B1...Bn> displays all unused theorems in theories B1...Bn or their parents, but not in A1...Am or their parents.*)

section{* Sledgehammer *}
sledgehammer_params [provers = "
  e cvc3 metis smt spass z3 z3_tptp remote_e_sine remote_vampire   
", slice=true, verbose=true, isar_proof=true, timeout=120]

(*remote_e_tofof remote_leo2 remote_satallax remote_snark remote_waldmeister*)

(*
sledgehammer supported_provers

metis  smt  alt_ergo  dummy_thf  e  leo2  satallax  spass  spass_new  spass_old
vampire  z3_tptp  cvc3  z3  remote_e  remote_e_sine  remote_e_tofof  remote_iprover
remote_iprover_eq  remote_leo2  remote_satallax  remote_snark  remote_vampire
remote_waldmeister  remote_z3_tptp  remote_cvc3  remote_z3
*)


end