tuned;

updated 'obtain';

Removed Quot

Never used and not relevant.

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

*** empty log message ***

tuned msg;

Corrected example which still used old primrec syntax.

Replaced force by fast because force may now take forever to fail (due to a recend change of David's)

new constant same_fst

by (CLASIMPSET auto_tac);

added clarify method; removed unofficial improper methods;

added clarsimp method;

tuned;

removed slow, slow_best methods; added clarify, clarsimp methods;

* Isar/Provers: intro/elim/dest attributes: changed intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one should have to change intro!! to intro? only);

rearranged setup of arithmetic procedures, avoiding global reference values;

lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);

do nat pass theory value, but sg_ref;

avoid referencing thy value; rename_numerals: use implicit theory context; eliminated some simpset_of Int.thy (why needed anyway?);

avoid referencing thy value; rename_numerals: use implicit theory context;

tuned deps;

tuned;

changed deps;

rename_numerals: use implicit theory context;

avoid referencing thy value; lemma_prat_add_mult_mono moved to PRat.ML;

avoid referencing thy value; lemma_prat_add_mult_mono moved here;

avoid referencing thy value; rename_numerals: use implicit theory context; avoid some simpset_of Int.thy (why needed anyway?);

simpset_of NatDef.thy (why anyway?);

avoid referencing thy value; rename_numerals: use implicit theory context;

avoid referencing thy value;

tuned comment;

avoid global references;

do not pass theory values, but sg_ref;

Drule.merge_rules;

get_names: topologically sorted;

removed all_sessions.graph; improved graph 'directories'; tuned;

removed all_sessions;

disallow duplicates in session identifiers;

assimilated;

tuned HeapFun;

tuned ThmHeap;

removed selector syntax -- improper tuples are broken beyond repair :-(

elim?;

classical atts now intro! / intro / intro?;

renamed "Directories" to "Sessions";

tuned;

improved error msg; thm foo.cases;

added ex_someI

much tidying in connection with the 2nd UNITY paper

strengthened force_tac by using new first_best_tac

removed safe_asm_full_simp_tac

added map_upd_nonempty, also to simpset

removed weaker variant of subset_insert_iff

removed safe_asm_full_simp_tac, added generic_simp_tac

Updating of some comments

*** empty log message ***

Univ no longer requires Arith (really it never did)

tuned;

corrected header

changed / to // for quotienting

changed / to // for quotienting; general tidying

renamed // to / (which is what we want anyway) to avoid clash with the new use of // for quotienting

deleted redundant proof

// change; also moved entry for AddIffs

addsplits [split_if];

theorems foo.splits = foo.split foo.split_asm;

removed obsolete expand_if = split_if;

* HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm;

* HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm; datatype package provides theorems foo.splits = foo.split foo.split_asm for each datatype;

replaced arities by instance;

MicroJava structure changed

consts: include *all* names;

tuded presentation;

AddXIs [UnI1, UnI2];

flat instruction set, op. semantics now in JVMExecInstr.thy

flat instruction set

10pt

- xsymbols for \<noteq> \<notin> \<in> \<exists> \<forall> \<and> \<inter> \<union> \<Union> - vector space type of {plus, minus, zero}, overload 0 in vector space - syntax |.| and ||.||

strip_prod_type = HOLogic.prodT_factors;

AST translation rules no longer require constant head on LHS;

fixed nested prod syntax;

use split_tupled_all;

use pair_tac; use split syntax;

adapted tuple syntax;

tuned;

use pair_tac;

use split syntax;

fixed tuple translations;

defs (overloaded);

added is_unitT; added proper versions of mk_tuple(T), dest_tuple(T) -- unused;

instance unit :: finite;

more robust tuple syntax (still improper, though!);

improved unit theory: unit_all_eq1, unit_all_eq2, split_all_tac; tuned;

added syntax for proper / improper selector functions;

tuned;

tuned;

avoid 'split';

added Tuple.thy;

added ex/Tuple.thy;

syntax (symbols) "op o" moved from HOL to Fun;

added finite_unit;

AST translation rules no longer require constant head on LHS;

* tuned AST representation of nested pairs, avoiding bogus output in case of overlap with user translations (e.g. judgements over tuples); * AST translation rules no longer require constant head on LHS;

corrections (cast relation, Prog.ML -> Decl.ML)

improved add_edges_cyclic;

re-structuring MicroJava; added Example; corrected := syntax; simplfied cast

added (surjective_pairing RS sym) to simpset

strengthened rtranclD

added option_map_o_sum_case (also to simpset)

added sum_case_empty_empty (also to simpset)

tuned syntax

added hint on fun_sum

added fun_upd2_simproc

re-added subset_empty to simpset

used bounded quantification in definition of guarantees and other minor adjustments

moved sublist from UNITY/AllocBase to List

AddIffs

parent should be Main

changed the quotient syntax from / to //

tuned cycle_msg;

updated;

HOL: the disjoint sum is now "<+>" instead of "Plus"; ML: PureThy.add_defs gets additional argument;

adapted PureThy.add_defs_i;

defs (overloaded);

tuned;

added read_xnum;

fix(_i): admit internal variables;

use ProofContext.bind_skolem;

defs: (overloaded) option;

eq_prop: strip_assums_concl;

tuned exceptions; added add_deps_acyclic, merge_acyclic;

const_deps: unit Graph.T; proper merge of const_deps; tuned;

add_term_consts: ins_string;

add_defs(_i): overloaded option;

adapted PureThy.add_defs;

fixed comment;

adapted PureThy.add_defs_i;

use Syntax.read_xnum;

fixed simplified_cases;

fixed name: UN_empty3;

replaced infix Plus by <+>;

removed duplicate Compl_atMost;

fixed compose decl;

defs: (overloaded) option;

method cases/induct: (opaque) option;

defs (overloaded);

removed now-redundant proof steps

added an important default rule

fixed a failing proof

le_refl_iff as default rule

removed needless premises

AddIffs now available for FOL, ZF

added simp_case_tac; proper handling of case names with simplification; support "(opaque)" mode; tuned;

use InductMethod.simp_case_tac;

tuned;

export thesisN separately;

prep rhs in original context; tuned;

RuleCases.make opaq;

bind_skolem;

invoke_case: bind_skolem;

"_i" arguments now expected to have skolems already internalized; removed unused cert_skolem, export intern_skolem, added bind_skolem;

make: opaq flag;