axiomatization: declare Spec_Rules, direct result;

use simultaneous Morphics.fact;

primitive defs: clarified def (axiom name) vs. description;

eliminated obsolete thm position tags;

permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);

provide actual Nitpick_HOL.extended_context;

tuned;

more accurate dependencies;

eliminated obsolete CVS Ids; tuned headers;

merged

added benchmark for large records

merged

clarified quick-and-dirty usage in record package; removed non-optimized versions of proofs; introduced future proofs

simplified bulky metis proofs;

properly inlined @{lemma} antiqutations -- might also reduce proof terms a bit;

moved old SList, LList, LFilter to AFP/Lazy-Lists-II;

include HOL-Boogie keywords by default;

eliminated obsolete CVS Ids; tuned headers;

updated keywords;

generate keywords for Emacs Proof General only; tuned;

dismantled remains of old jEdit plugin;

isabelle_document: more explicit error output, notably for drafts;

LocalTheory -> Local_Theory

merged

automate definition of representable domains from algebraic deflations

cleaned up, removed unneeded call to Syntax.check_term

merged

moved lemma from Algebra/IntRing to Ring_and_Field

merged

merged

-

updated Local_Theory and Theory_Target;

modernized structure Local_Theory;

eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;

inductive: eliminated obsolete kind;

merged

A little rationalisation

eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);

merged

removed unused code and unused arguments, tuned

adapted proofs due to changes in HOL-Boogie

parallel solving of Boogie splinters

corrected translation of integer operators, keep argument order for n-ary symbols (conjunction, disjunction), removed unused code

extended theory simpset to simplify non-linear problems

more "anti_sym" -> "antisym" (cf. a4179bf442d1);

merged

renamed lemmas "anti_sym" -> "antisym"

a few lemmas for point-free reasoning about transitive closure

merged

A number of theorems contributed by Jeremy Avigad

merged

merged

adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes

removed annoying tracing message

added a tabled implementation of the reflexive transitive closure

merged

merged

improved ML interface to pcpodef

use Drule.standard (following typedef package), add pcpodef tactic interface

eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";

eliminated obsolete "internal" kind -- collapsed to unspecific "";

unused_thms: ignore kind -- already observes "concealed" flag;

all_valid_thms: more sophisticated check against global + local name space;

Remove map_compose, replaced by map_map

New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key

Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute

merged

accomplish mutual recursion between fun and inst

moved lemma map_of_zip_map to Map.thy

merged

explicit code lemmas produce nices code

repaired broken code_const for term_of [String.literal]

fixed soundness bug in Nitpick related to sets

removed unnecessary oracle in the predicate compiler

improving code quality thanks to Florian's code review

renaming code_pred_intros to code_pred_intro * * * adopted alternative definitions for the predicate compiler to new attribute name

announcing the predicate compiler in NEWS and CONTRIBUTORS

new names for predicate functions in the predicate compiler * * * adopting examples of the predicate compiler

removed deprecated mode annotation parser; renamed accepted mode annotation parser to nicer naming

added another example to the predicate compiler * * * tuning examples

changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned

removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main

adopted predicate compiler examples to new syntax for modes

added interface of user proposals for names of generated constants

first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes

adding more tests for the values command; adding some forbidden constants to inductify * * * added further testcase for values command

Enables tests for locale functionality that is now available.

merged

uniform use of simultabeous use_thys;

merged

explicit invocation of code generation

adding code equations for constructors

tuned

changed URL of SMT server, added Z3 rewrite lemma

Added two new lemmas

tuned imports

tuned

local mutex for theory content/identity operations;

admit dummy implementation;

Toplevel.thread provides Isar-style exception output;

generalized Runtime.toplevel_error wrt. output function;

exported SimpleThread.attributes;

plain add_preference, no setmp_CRITICAL required;

adapted Theory_Data;

recovered update from 7264824baf66, which got lost in 7264824baf66;

merged

merged

tuned header

substantial simplification restores code generation

lemmas about apfst and apsnd

tuned imports

merged

HOLCF example: domain package proofs done manually

add lemma parallel_fix_ind

add title/author block

theory of representable cpos

add map_map lemmas

add in_deflation relation, more lemmas about cast

ep_pair and deflation lemmas for powerdomain map functions

remove spurious parameter to "merge"