%h1= @page_title = t('proofs.new.title', klass: klass, resource: resource)
- if proving_single_theorem?
%h2= t("proofs.new.theorem_definition")
- else
%h2= t("proofs.new.theorems_definitions")
%thead
%tr
%th= t('theorems.index.name')
%th= t('theorems.index.text')
%tbody
- theorems.each do |theorem|
= render partial: 'theorems/theorem_large', locals: {resource: theorem}
%h2= t('proofs.new.configuration')
= simple_form_for resource, url: url_prove_form do |f|
= f.input :prover_ids, label: t('proofs.new.provers.label'), collection: ontology.current_version.provers, label_method: :to_s, as: :check_boxes, hint: t('proofs.new.provers.none_is_default')
.col-lg-2
= link_to t('proofs.new.provers.select_all'), '#', class: 'btn btn-xs btn-default', data: {select: '#prover-list :checkbox', select_target: 'all'}
= link_to t('proofs.new.provers.select_none'), '#', class: 'btn btn-xs btn-default', data: {select: '#prover-list :checkbox', select_target: 'none'}
= f.input :timeout, label: t('proofs.new.timeout.label'), collection: Proof::TIMEOUT_RANGE, label_method: ->(value) { proof_timeout_label(value) }, hint: t('proofs.new.timeout.hint'), input_html: {class: 'timeout'}, include_blank: t('proofs.new.timeout.default')
.columnized-items
= f.input :axiom_selection_method, label: t('proofs.new.axiom_selection.method'), collection: AxiomSelection::METHODS, as: :radio, include_blank: false, label_method: ->(value) { t("axiom_selection.#{value}") }, checked: checked_axiom_selection_method
#axiom-selection
= render partial: 'axiom_selection/manual_axiom_selection', locals: {f: f, ontology: ontology}
= render partial: 'axiom_selection/sine_axiom_selection', locals: {f: f}
= f.button :submit, t('proofs.new.send'), class: 'btn btn-primary'