obtain;

added split_bind_asm, bind_splits;

adapted obtain; tuned;

removed equalityCE;

added atomic_Trueprop;

updated ObtainFun;

'def': no constraint on variable;

exporter setup for context elements;

export RANGE, hard_asm_tac, soft_asm_tac; export is_chain, assert_forward_or_chain; added the_fact; updated ProofContext.export_wrt;

turned into plain context element; exporter setup;

local_def(_i): no constraint on var; exporter setup;

local_def(_i): no constraint on var;

def: no constraint on var;

added is_judgment; removed atomic_thesis;

ObtainFun (generalized existence reasoning);

ThmDeps.enable;

added sign_of_cterm;

Logic.goal_const;

replaced "Sessions" by "Root";

apply. -> by

* HOL/While

added theory While;

export has_internal; tag some rules as internal;

added thm_deps;

added enter_forward_proof;

export write_graph;

begin_theory: store *copy* of initial theory;

tuned;

intro_elim_tac: bimatch_from;

While functional for defining tail-recursive functions