added chained_goal, which presents the goal thm as seen by semi-structured methods;

tuned;

removed dead/duplicate code;

aliases for Thomas Sewell;

modernized Balanced_Tree;

replaced meta_iffD2 by existing Drule.equal_elim_rule2; replaced SymSymTab by existing Symreltab; more antiquotations; eliminated old-style Library.foldl, Library.foldl_map; tuned;

tuned header;

Thomas Sewell, NICTA: more efficient HOL/record implementation;

tuned whitespace -- recover basic Isabelle conventions;

merged

Merge with isabelle dev changes.

Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.

Avoid a possible variable name conflict in instantiating a theorem. Instantiating a theorem variable with new variables created a possible variable name conflict if a record was defined with a field named 'f', 'x' etc. Using variable indices of 1 avoids the problem.

Fix unescaped expressions breaking latex output in Record.thy Expressions containing _ and ^ need to be adjusted or antiquoted in text comments for latex compatibility. This is in fact a little annoying, since it makes the comment less readable in both source and HTML form.

Merge record patch with updates from isabelle mainline.

Avoid record-inner constants in polymorphic definitions in Bali The Bali package needs to insert a record extension into a type class and define an associated polymorphic constant. There is no elegant way to do this. The existing approach was to insert every record extension into the type class, defining the polymorphic constant at each layer using inner operations created by the record package. Some of those operations have been removed. They can be replaced by use of record_name.extend if necessary, but we can also sidestep this altogether. The simpler approach here is to use defs(overloaded) once to provide a single definition for the composition of all the type constructors, which seems to be permitted. This gets us exactly the fact we need, with the cost that some types that were admitted to the type class have no definition for the constant at all.

Merge with changes from isabelle dev repository.

Initial response to feedback from Norbert, Makarius on record patch As Norbert recommended, the IsTuple.thy and istuple_support.ML files have been integrated into Record.thy and record.ML. I haven't merged the structures - record.ML now contains Record and IsTupleSupport. Some of the cosmetic changes Makarius requested have been made, including renaming variables with camel-case and run-together names and removing the tab character from the Author: line. Constants are defined with definition rather than constdefs. The split_ex_prf inner function has been cleaned up.

Branch merge for isabelle mainline updates.

Branch merge with updates from mainline isabelle.

Implement previous fix (don't duplicate ext_def) correctly.

There's no particular reason to duplicate the extension constant's definition under the name "ext_def", and it also prevents you having a field called ext.

Merged with mainline changes.

Adjust some documentation.

Simplification of various aspects of the IsTuple component of the new record package. Extensive documentation added in IsTuple.thy - it should now be possible to figure out what's going on from the sources supplied.

Record patch imported and working.

Initial attempt at porting record update to repository Isabelle.

Synchronized and Unsynchronized;

hide "ref" by default, to enforce excplicit indication as Unsynchronized;

explicit indication of Unsynchronized.ref;

open_unsynchronized for interactive Isar loop;

explicit indication of Unsynchronized.ref;

Raw ML references as unsynchronized state variables.

Dummy version of state variables -- plain refs for sequential access.

reactivated at-sml-dev-e;

misc tuning and modernization;

moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);

merged

less auxiliary functions

tuned

shared code between rep_datatype and datatype

further unification of datatype and rep_datatype

avoid compound fields in datatype info record

fold_body_thms: pass pthm identifier; fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen"; fulfill_proof/thm_proof: check for thm cycles at the substitution point;

tuned internal source structure;

added fork_deps_pri;

merged

explicit pointless checkpoint

emerging common infrastructure for datatype and rep_datatype

streamlined rep_datatype further

simplified rep_datatype

more appropriate order of field in dt_info

re-established reasonable inner outline for module

merged

adjusted to changes in datatype package

merged

dropped dead code

registering split rules and projected induction rules; ML identifiers more close to Isar theorem names

fold_body_thms/join_bodies: explicitly check for cyclic theorem references;

tuned;

reachable: recovered reverse post-order (lost in 73ad4884441f), which is expected for all_preds/all_succs and required for topological_order;

merged

New lemmas involving the real numbers, especially limits and series

NEWS; corrected spelling

merged

simplified proof

removed potentially dangerous rules from pred_set_conv

explicitly hide empty, inter, union

merged

merged

merged

inf/sup_absorb are no default simp rules any longer

merged

merged

adapted proof

merged

tuned proofs

tuned header

added note on simp rules

merged

tuned proof; tuned headers

merged

tuned proofs; be more cautios wrt. default simp rules

merged

tuned proofs

merged

inter and union are mere abbreviations for inf and sup

merged

lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup

subsumed by more general setup in List.thy

idempotency case for fold1

added dual for complete lattice

merged

record how many "proof"s are solved by s/h

added quotes for filenames; truncated remaining time (no floats supported by ulimit)

merged; adopted to changes from Code_Evaluation in the predicate compiler