proper theory_long_name;

clarified signature: explicitly distinguish theory_base_name vs.

more operations, following Isabelle/ML conventions;

tuned;

clarified theory_id: plain value without state;

merged

no "open" of ML structures: it makes sources unmaintainable;

adapted to Isabelle/f4cd6e3b5075;

adapted to Isabelle/5db014c36f42;

adapted to Isabelle/5db014c36f42;

This file should have been removed in the previous commit.

Sync with my development repo. Main changes related to…

tuned

clarified terminology

minor performance tuning: recursive check of pointer_eq;

minor performance tuning: avoid excessive (de)constructions for base cases;

tuned;

unused (see also 864c7c684651 and b6aa5eac0a1a);

tuned;

discontinued somewhat pointless operation: Conjunction.intr_balanced /…

more operations: avoid intermediate list;

update NEWS: Sortset and Termset turned out to be counter productive, Ord_List.

tuned;

drop unused Set().ord, which is potentially inefficient due to dict_ord/dest;

tuned;

Thm.shared context: speed-up low-level inferences;

backout b6aa5eac0a1a;

tuned whitespace;

backout 4a174bea55e2;

Backed out changeset f34d11942ac1

backout e3fe192fa4a8;

Backed out changeset e3db27e3b0c6

backout 61f652dd955a;

Backed out changeset cd5d56abda10

revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;

eliminated pointless parallelism: approx. 1.3s as plain sequential ML;

update timing;

tuned;

alternative version by Manuel Eberl, following the approach of…

adapted to Isabelle/c274f52b11ff;

Backed out changeset a537fb4c92af

slightly faster thanks to Thm.shared_context from Isabelle/4f9117e6020d;

merged

moved lemma to FDS exercises

Fix proofs broken by previous commit.

Add congurence rule for bind_tm in Root_Balanced_Tree.Time_Monad

tuned;

tuned;

eliminated aliases: prefer existing Thm.elim_implies;

more standard use of structure Unsynchronized;

tuned;

tuned whitespace;

not unused!

Added running time analysis

merged

tuned;

merged

code_target: create subdirectories for export_code file

minor performance tuning: more elementary operations;

clarified signature: support "suppress" prefix as int, followed by list;

tuned signature;

minor performance tuning: more elementary operations;

tuned signature;

more operations;

more direct hg_sync init via ssh (see also 721b3278c8e4);

tuned;

more operations;

tuned: more direct re-use;

more direct clone (see also change of exception in 8d8c70b41bab);

more operations, following Isabelle/ML conventions;

more operations, following Isabelle/ML conventions;

proforma use of Long_Name.chunks, without change of the representation of…

merged

compact representation of long name "chunks", with bitmask to suppress elements…

minor performance tuning;

misc tuning and clarification;

clarified signature;

more compact: avoid redundant entries;

tuned;

tuned;

more operations;

performance tuning: proper pointer_eq;

added lemmas multpHO_repeat_mset_repeat_mset[simp] and multpHO_double_double…

merged

added lemma multp_image_mset_image_msetI

merged

proper invariants

tuned signature;

misc tuning: follow Table() more closely;

merged

performance tuning: replace Ord_List by Table();