Index
- !(T)
- ---> Names
- ;(T, U)
- =(Term1, Term2)
- Annotations on proof nodes
- Concepts
- Constraints on rules
- Ergo5 types
- General commands (viewing data and setting parameters)
- Gumtree Tactics
- I/O Syntactic Sugar Commands.
- Miscellaneous Commands.
- Modes and Types
- Name doc DocStrings extends Nodes.
- Parameters
- Proof File Properties
- Proof Information Commands
- Proof Tree Commands
- Proof commands (The 'GumTree' User Interface for Ergo 5 proofs)
- Query Language for Rules
- Query Procedures
- Rule context specification
- Rule/Tactic Table Commands
- Save/Close/Read Proof Commands
- Save/Exit Commands.
- Table Commands
- Tactic Combinator Commands
- Tactic File Commands.
- Theory Construction Commands.
- Theory Deletion Commands.
- Theory Extension Commands.
- Theory Search List
- Theory/Database Commands (The DBMS user interface)
- User Defined Gumtree Tactics
- User Defined Tables
- User Defined Tactic Tables
- Variable Instantiation Commands
- Writelists
- [T1,T2,...]
- [Thy].
- abandon
- abbreviation E === I.
- add_abbrevs(Thy)
- add_context_name(Name)
- add_global_tactic_file(File)
- add_hyp(Tactic)
- add_hyp(Tactic, Result, Hyp)
- add_hyp_ante(Tactic, Ante)
- add_hyp_ante(Tactic, Result, Ante, Hyp)
- add_hyp_f(Tactic)
- add_hyp_f(Tactic1, Tactic2)
- add_hyp_f(Tactic1, Tactic2, Result, Hyp)
- add_operator(Prec, Kind, Name)
- add_operators(Thy)
add_all_operators(Thy)
- add_subtheory(S)
- add_tactic_file(File)
add_tactic_file(File, Thy)
- add_theory(T)
- add_visible_theory(Thy)
- annotate(L)
- annotate(PNode, Ann)
- annotate(PNode, Ann)
- annotation(PNode, Ann)
- annotations(PNode, AnnList)
- anyvar
- atom
- atom(A)
- atomic
- axiom Name === RHS
- batch_mode
- bool
- bye
- cdiff
- chars
- close_theory
- close_win
- cmd
- cmdtab
- cname
- code
- commit(CmdNum)
commit(CmdNum, Label)
- compile_global_tactic_file(File)
- compile_tactic_file(File)
compile_tactic_file(File, Thy)
- compound
- constraints(Vars, Dist, NFI, Other)
- context(K, N, T)
- context_assume(CName, PNode, CId, CTerm)
- context_diff(PNode, Ancestor, CName, CDiff)
- context_diff_to_spec(CDiff, VarMap, CSpec)
- context_index(CName, PNode, Index, CId)
- context_index(K, I, CId)
- context_nfi(ObVar, PNode)
- context_search(CName, PNode, CId, CTerm)
- context_terms(T)
- cspec
- cterm
- ctermid
- deabbrev(T)
- deabbrev_and_call_gumtree_tactic(T)
- deabbrev_focus
- declare Symbol.
- declare(Name,Arity).
- declare_object_vars(A)
- declare_param_const(Name, Value, Check)
- declare_table Decl
- declare_tactic_table Decl
- define F === Term.
- defined(D, E)
- delay_until(Condition, Constraints)
- delete_abbrev(Abbrev)
delete_abbrev(Abbrev, Term)
- delete_abbrevs(Thy)
- delete_operator(Name)
delete_operator(Name, Kind)
- delete_operators(Thy)
- delete_subtheory(S)
- delete_theory(T)
- delete_theory_and_dependents(T)
- delete_visible_theory(Thy)
- dependent_rules(Rules, Dependents)
- docnode
- elves_type
- emptylist
- enable_abbreviation
disable_abbreviation
- ensure_loaded_global_tactic_file(File)
- ensure_loaded_tactic_file(File)
ensure_loaded_tactic_file(File, Thy)
- erase_table(Name)
- erase_tactic_table(Name)
- exec_gumtree_tactic(T)
- fail
- fails(T)
- filename
- fix(N)
- focus(F)
- gcomp
- ground
- gumtree_display
- help
- help Topic
help(Topic, Thy)
- history
- html_doc_clear_memory
- html_doc_tree(Dir, RootList)
- if_tac(Cond, Then, Else)
- in_table(Name, Term1, Term2)
- in_tactic_table(Name, Tactic)
in_tactic_table(Name, Tactic, Term)
in_tactic_table(Name, Tactic, Term, Arg)
- include_theory(Thys)
include_theory(Thys, Syntax)
- inherit_all_operators(Thy)
- inherit_all_visible_theories(Thy)
- inherit_theory(Thy)
- instantiate(Abs, Sub, Inst, Repar, Subint)
- integer
- integer(I)
- interpret(Abs, Sub, Inst, Repar, Subint)
- irules(Query)
- is_disabled_rule(Thy, Rule)
- is_not_free_in(Obvar, Term)
- iuse(Query)
- iuse(Query, Output)
- list(Type), openlist(Type)
- load_global_tactic_file(File)
- load_path
- load_tactic_file(File)
load_tactic_file(File, Thy)
- macro_and_delete(File)
macro(File)
- msg(Caller, Msg)
msg(Caller, Level, Msg)
- name(N)
- names(L)
- new_annotation(Type, Doc)
- nodeid
- nonvar
- not_free_in(Obvar, Term)
- number
- obvar
- oh(Hyp)
- oh(NewHyp, OldHyp)
- one
- op(PosList)
- premises(Prems)
- proof_complete(Name, Root, OpenNodes, Constraints)
- proof_complete_postulate(Root)
proof_complete_postulate(Root, Unproved)
- proof_constraints(Nodes, Dist, NFI, User, Context)
proof_constraints(Root, Vars, Dist, NFI, User, Context)
- proof_disable_rules(Rules)
- proof_new_node(Id, Parent, Term)
- proof_node_children(Id, Children)
- proof_node_context(Id, Contexts)
- proof_node_parent(Id, Parent)
- proof_node_rule(Id, Thy, Rule, RuleType)
- proof_node_rule_and_children(Id, Thy, Rule, RuleType, Children)
- proof_node_term(Id, Pred)
proof_node_terms(Ids, Preds)
- proof_node_timestamp(Node, Timestamp)
- proof_open_nodes(Id, OpenNodes)
- proof_root(Node)
- proof_root_postulate(Node, Thy, Name)
- proof_root_sequents(Sequents)
- proof_start(Formula, Constraints, Children)
- proof_start_postulate(Name, Children)
- proof_step(Thy, Rule, Id, Children)
- proof_tactic(Ann, NameMap, Root, Tac)
- proofnode
- prooftreeIDs(Root, Tree)
- prove(Pred)
- prove_rule(Name)
prove_rule(Name, Concl)
- quant
- quit_proof
- quit_proof
- read_proof(RuleName, Version, Tac, Properties)
read_proof_file(File, Version, Tac, Properties)
- real
- recompile_all_tactic_files
- recompile_global_tactic_file(File)
- recompile_tactic_file(File)
recompile_tactic_file(File, Thy)
- reconsult_global_tactic_file(File)
- reconsult_tactic_file(File)
reconsult_tactic_file(File, Thy)
- require_global_tactic_file(File)
- require_tactic_file(File)
require_tactic_file(File, Thy)
- rerun_all_postulate_proofs
- rerun_postulate_proof(RuleName)
- rerun_proof(RuleName)
- rerun_proof(RuleName)
- rerun_proof_file(File)
- resume
- retry
- reverseRel
- rootnode
- rule(R)
- rule_add(Name, Concl, ConclId, SeqList, Constraints)
- rule_make_fundamental(Name)
- rulename
- rules(Query)
- runtime
- save
- save_postulate_proof(Root)
- save_proof(Name, Root)
save_proof(Name, Root, OpenNodes, Constraints)
- save_proof_to_file(Thy, Name, Node, OpenNodes, Constraints)
- save_snapshot(File)
- set Parameter === Value
- shell(String)
- show
- show(Topic)
- show(Topic, Thy)
- show_annotations(Ids)
- show_constraints
show_constraints(Vars)
- show_context(Id)
- show_dependent_rules(Rules)
- show_node(Id)
- show_node_and_context(Id)
show_nodes_and_context(Ids)
- show_open_nodes
show_open_nodes(Id)
- show_open_nodes_and_context
show_open_nodes_and_context(Id)
- show_proof(RuleName)
show_proof_file(File)
- show_proof_script(RuleName)
show_proof_script_file(File)
- show_prooftree(Root)
- show_prooftree_tactic(Root)
- show_rule(Rule)
show_rule(Rule, Kind)
show_rule(Name, Thy, Kind)
- show_subproof(Node)
- show_subproof_script(Node)
- show_table(Table)
- show_tables
- show_tactic(Anns, Tac)
- show_tactic_script(Tac)
- show_tactic_table(Table)
- show_tactic_tables
- silent_cmd(Cmd)
- simplify_substitutions
- skip
- srule(R)
- start_wi
- start_window_proof
- statistics
- stop_wi
- stop_window_proof
- stream
- strongerRel
- succs(T)
- symbols
- table(Name, Term1, Term2)
- tactic
- tactic Decl
- tactic_annotations(Tac, Patt, Anns)
- tactic_table(Name)
- tactic_table(Name, Val)
- term
- term(T)
- terms(L)
- theorem Name === RHS
- theorem_action
- theorem_constraints(Vars, Dist, NFI, Others)
- theory
- thy(Type)
- touch_theory(Thy)
- trace
trace(Caller)
trace(Caller, Level, Msg)
- trans(Tactic)
- trans(Tactic, Result)
- trans_ante(Tactic, Ante)
- trans_ante(Tactic, Result, Ante)
- trans_def_f
- trans_def_f(Result)
- trans_def_r
- trans_def_r(Result)
- trans_f(Tactic)
- trans_f(Tactic, Result)
- trans_f_ante(Tactic, Ante)
- trans_f_ante(Tactic, Result, Ante)
- trans_r(Tactic)
- trans_r(Tactic, Result)
- trans_r_ante(Tactic, Ante)
- trans_r_ante(Tactic, Result, Ante)
- trans_rt(Tactic)
- trans_rt(Tactic, Result)
- trans_rt_ante(Tactic, Ante)
- trans_rt_ante(Tactic, Result, Ante)
- trans_rule(Tactic)
- trans_t(Tactic)
- trans_t_ante(Tactic, Ante)
- two
- undo
- undo(CmdNum)
- use(Query)
- use(Query, Output)
- usercmd(CmdNum, Node, InNodes, OutNodes, Cmd)
- var
- verbosity
- with_context_delaying(Code)
with_context_delaying(Patt, Code)
- with_context_delaying(Patt, T)
- write_depth
- write_proof_file(File, PNode, Properties)
- writelist
- zero
- {G}
- |(T, U)
