print_theorems: more robust difference, even after finished proof;

export context_node;

merged

more antiquotations;

pcpodef package: state two goals, instead of encoded conjunction;

recovered goal_pat;

inhabitance goal is now stated in original form and result contracted -- the previous attempt with contracted goal and initial unfolding did not work, because it disrupted the Isar proof structure (e.g. ?thesis);

tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.; more antiquotations; explicit Theory.requires; adapted to recent changes in ~~/src/HOL/Tools/typedef_package.ML; misc tuning and simplification;

add_typedef: unfold set_def in tactical proof as well;

merged

Theory.checkpoint before commencing proof;

misc tuning and modernisation;

merged

logically separate typedef axiomatization from constant definition

add def before setting up goal

killed dead code

constrain type inference to sort "type"

merged.

cleaned up some proofs in Cfun.thy

implement cont_proc theorem cache using theory data

use ML antiquotations

clean up diff_bin_simps

move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs

fixed import: requires ContNotDenum;

fixed import: requires ContNotDenum;

requires RComplete;

merged.

move all neg-related lemmas to NatBin; make type of neg specific to int

separate neg_simps from rel_simps

use {less,le}_number_of in integer simprocs