tuned

--HG--
extra : rebase_source : 97084c84459c3dd34cf5eccbce5df53a905229de

tuned signature;

clarified sessions/directories;

setup preprocessing for HOL proofs;

early setup of proof preprocessing;

prefer named lemmas -- more compact proofterms;

tuned;

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);

tuned "=" syntax declarations; made "~=" uniformly "infix"

A few new results, elimination of duplicates and more use of "pairwise"

added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly

--HG--
rename : src/HOL/Library/FuncSet.thy => src/HOL/FuncSet.thy

new material on matrices, etc., and consolidating duplicate results about of_nat

lots of new material, ultimately related to measure theory

standardized towards new-style formal comments: isabelle update_comments;

uniform use of Standard ML op-infix -- eliminated warnings;

ran isabelle update_op on all sources

prefer formal citations;
more accurate bibtex entries;

prefer control symbol antiquotations;

more symbols;

derived axiom iffI as a lemma (thanks to Alexander Maletzky)

tuned imports

--HG--
extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011

proper concept of code declaration wrt. atomicity and Isar declarations

--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472

added simp rules

clarified notation: iterated quantifier is negated as one chunk;

clarified notation;

misc tuning and modernization;

add lemmas contributed by Peter Gammie

Type_Infer.object_logic controls improvement of type inference result;

eliminated unused simproc identifier;

abbreviations for \<nexists>;

old HOL syntax is for input only;

more canonical names

eliminated old defs;

former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";

discontinued ASCII replacement syntax <->;

stripped some legacy

--HG--
extra : rebase_source : 6eb5300f527881549c97b95d7e61a2275f3509a7

isabelle update_cartouches -c -t;

discontinued specific HTML syntax;

isabelle update_cartouches;

Added new simplifier predicate ASSUMPTION

tuned proofs -- less legacy;

simplified simproc programming interfaces;

eliminated \<Colon>;

updated to infer_instantiate;
tuned;

proper LaTeX;

more symbols;

isabelle update_cartouches;

undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)

swap False to the right in assumptions to be eliminated at the right end

undid 6d7b7a037e8d

new ==> simp rule

added simp rules for ==>

clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);

proper context for Object_Logic operations;

local setup of induction tools, with restricted access to auxiliary consts;
proper antiquotations for formerly inaccessible consts;

tuned;

added lemmas

fix parameter order of NO_MATCH

clarified context;
tuned;

Thm.cterm_of and Thm.ctyp_of operate on local context;

clarified signature;

tuned signature -- prefer qualified names;

New lemmas and a bit of tidying up.

misc tuning;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

named_theorems: multiple args;

proper context for assume_tac (atac remains as fall-back without context);

proper context;

proper context for match_tac etc.;

proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

modernized header uniformly as section;

eliminated aliases;

disable coercions for NO_MATCH

modernized setup;

move NO_MATCH simproc from the AFP entry Graph_Theory to HOL

Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;

updated to named_theorems;

updated to named_theorems;

updated to named_theorems;

modernized module name and setup;

reduced name variants for assoc and commute on plus and mult

tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";

use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges

prefer proof context over background theory

--HG--
extra : rebase_source : 307a2e54d5c0b89d8668ce99110df0538037668e

modernized tool setup;
tuned;

discontinued axiomatic 'classes', 'classrel', 'arities';

more explicit axiomatization;

more standard file/module names;

--HG--
rename : src/HOL/Tools/cnf_funcs.ML => src/HOL/Tools/cnf.ML
rename : src/HOL/Tools/sat_funcs.ML => src/HOL/Tools/sat.ML

fundamental treatment of undefined vs. universally partial replaces code_abort

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;

congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj

recover static nnf_ss from 6c0de045d127 -- avoid odd runtime warnings due to duplication of not_not;

hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

tuned message -- more markup;

standardized aliases;

syntax translations always depend on context;

uniform Proof.context for hyp_subst_tac;

simplifier uses proper Proof.context instead of historic type simpset;

tuned pretty layout: avoid nested Pretty.string_of, which merely happens to work with Isabelle/jEdit since formatting is delegated to Scala side;
declare command "print_case_translations" where it is actually defined;

discontinued obsolete ML antiquotation @{claset};

just one HOLogic.Trueprop_conv, with regular exception CTERM;
tuned;

marginalized historic strip_tac;

check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop

--HG--
extra : rebase_source : d3377cc95a6a398ca555e30fab13d69b288cb6d8

separate data used for case translation from the datatype package

\<noteq> now has the same associativity as ~= and =

eliminated some old material that is unused in the visible universe;

prefer ML_file over old uses;

faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

removed obsolete rev_contrapos (cf. 1d195de59497);

prefer sys.error over plain error in Scala to avoid deprecation warning

moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator

--HG--
extra : rebase_source : b076bdc988c7c7c0c677783ce48cd24025a8d5d6

modernized axiomatization;
eliminated odd 'finalconsts';

declare command keywords via theory header, including strict checking outside Pure;

renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;

more conventional eval_tac vs. method_setup "eval";
clarified method "normalization": THEN_ALL_NEW avoids bumping into other subgoals;

prefer antiquotations;

improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
tuned;

more antiquotations;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

eliminated obsolete "standard";

tuned Named_Thms: proper binding;

replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed

removing old code generator setup in the HOL theory

modernized structure Induct_Tacs;

New proof method "induction" that gives induction hypotheses the name IH.

tuned proofs

moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace

old term operations are legacy;

removing the SML evaluator

install case certificate for If after code_datatype declaration for bool

tuned signature;

ML antiquotations are managed as theory data, with proper name space and entity markup;
clarified Name_Space.check;

simplified BLAST_DATA;

modernized functor names;
tuned;

clarified map_simpset versus Simplifier.map_simpset_global;

simplified Blast setup;

misc tuning and simplification;

proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;

modernized Quantifier1 simproc setup;

clarified simpset setup;
discontinued unused old-style FOL_css;

explicit context for Codegen.eval_term etc.;

making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement

eliminated Codegen.mode in favour of explicit argument;

modernized structure Proof_Context;

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

corrected infix precedence for boolean operators in Haskell

more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;

declare ext [intro]: Extensionality now available by default

setup case_product attribute in HOL and FOL

renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics

CRITICAL markup for critical poking with unsynchronized references;

avoid slightly odd Conv.tap_thy

replaced command 'nonterminals' by slightly modernized version 'nonterminal';

simplified evaluation function names

load "try" after "Metis" and move "Async_Manager" back to Sledgehammer

--HG--
rename : src/HOL/Tools/async_manager.ML => src/HOL/Tools/Sledgehammer/async_manager.ML

moved bootstrap of type_lifting to Fun

replace `type_mapper` by the more adequate `type_lifting`

--HG--
rename : src/HOL/Tools/type_mapper.ML => src/HOL/Tools/type_lifting.ML

setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;

simplified HOL.eq simproc matching;

file for package tool type_mapper carries the same name as its Isar command

--HG--
rename : src/HOL/Tools/functorial_mappers.ML => src/HOL/Tools/type_mapper.ML

lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;

module for functorial mappers

reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)

backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).

corrected OCaml operator precedence

comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)

Pure equality is a regular cpde operation

adjusted to changes in Code_Runtime

dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;

introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy

Code_Runtime.value, corresponding to ML_Context.value

code_eval renamed to code_runtime

--HG--
rename : src/Tools/Code/code_eval.ML => src/Tools/Code/code_runtime.ML

replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references

added Auto Try to the mix of automatic tools

Haskell == is infix, not infixl

more antiquotations;

use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
this *really* speeds up things -- HOL now builds 12% faster on my machine

avoid cyclic modules

normalization is allowed to solve True

normalization fails on unchanged goal

tuned text segment

finish moving file

fiddling with "try"

hide all-too-popular constant name eq

formerly unnamed infix equality now named HOL.eq

renamed class/constant eq to equal; tuned some instantiations

formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

formerly unnamed infix impliciation now named HOL.implies

prevent line breaks after Scala symbolic operators

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

discontinued obsolete 'global' and 'local' commands;

refined and unified naming convention for dynamic code evaluation techniques

deglobalized named HOL constants

tuned declaration order

qualified constants Let and If

optional break

moved misc legacy stuff from OldGoals to Misc_Legacy;
OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;

dropped superfluous [code del]s

added code_simp infrastructure

dropped unused bindings

removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead

less pervasive names from structure Thm;

incorporated further conversions and conversionals, after some minor tuning;

just one version of Thm.unconstrainT, which affects all variables;
temporary workaround for Nbe.lift_triv_classes_conv;

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

induct_true_def and induct_false_def are already contained in induct_rulify_fallback.

locale predicates of classes carry a mandatory "class" prefix

proper context for mksimps etc. -- via simpset of the running Simplifier;

avoid popular infixes

renamed command 'defaultsort' to 'default_sort';

syntax precedence for If and Let

renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
less pervasive names;

removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;

added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

reintroduce efficient set structure to collect "no_atp" theorems

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

fix typo in "nitpick_choice_spec" attribute name (singular, not plural)

added support for "specification" and "ax_specification" constructs to Nitpick

modernized structure Object_Logic;

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

tuned hyp_subst_tac';

more antiquotations;

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;

Added setup for simplification of equality constraints in cases rules.

new theory Algebras.thy for generic algebraic structures

some syntax setup for Scala

tuned code equations

Added setup for simplification of equality constraints in induction rules.

boolean operators for scala

a primitive scala serializer

killed a few warnings

split off evaluation mechanisms in separte module Code_Eval

--HG--
rename : src/Tools/Code/code_ml.ML => src/Tools/Code/code_eval.ML

some rearangement of load order to keep preferences adjacent -- slightly fragile;

replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules

removed unused Quickcheck_RecFun_Simps;

modernized structure Reorient_Proc;
explicit merge of constituent functions, avoids exponential blowup when traversing the import graph;
adapted Theory_Data;
tuned;

modernized structure Context_Rules;

tuned code setup

modernized some structure names;

separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;

tuned code setup for primitive boolean connectors

turned off old quickcheck

renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"

Removal of the unused atpset concept, the atp attribute and some related code.

explicit indication of Unsynchronized.ref;

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);

added first prototype of the extended predicate compiler

experimenting to add some useful interface for definitions

added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently

moved eq handling in nbe into separate oracle

added further conversions and conversionals

renamed functor BlastFun to Blast, require explicit theory;
eliminated src/FOL/blastdata.ML;

renamed functor ProjectRuleFun to Project_Rule;
renamed structure ProjectRule to Project_Rule;

renamed functor InductFun to Induct;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

moved abstract algebra section to the end

tuned code annotations

code attributes use common underscore convention

more accurate certificates for constant aliasses

renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;

arbitrary farewell

modernized method setup;

added collection of simplification rules of recursive functions for quickcheck

"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".

merged module code_unit.ML into code.ML

rewrite op = == eq handled by simproc

itself is instance of eq

transferred code generator preprocessor into separate module

--HG--
rename : src/Tools/code/code_wellsorted.ML => src/Tools/code/code_preproc.ML

reimplement reorientation simproc using theory data

misc cleanup of auto_solve and quickcheck:
tools are in src/Tools and loaded uniformly in HOL;
preferences are configured in their proper place -- despite old misleading comments in the source;
use predefined preferences categories;
setmp preferences in-place;

generic postprocessing scheme for term evaluations

avoid local [code]

re-engineering of evaluation conversions

code generator bootstrap theory src/Tools/Code_Generator.thy

wrecked old code_funcgr module

Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;

Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.

Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.

Second try at adding "nitpick_const_def" attribute.
I don't know what happened the first time (change d8944fd4365e). It just vanished somehow.

Merge.

reduced confusion code_funcgr vs. code_wellsorted

Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.

moved generic intuitionistic prover to src/Tools/intuitionistic.ML;

moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;

--HG--
rename : src/Provers/coherent.ML => src/Tools/coherent.ML
rename : src/Provers/eqsubst.ML => src/Tools/eqsubst.ML
rename : src/Provers/project_rule.ML => src/Tools/project_rule.ML

experimental switch to new well-sorting algorithm

formal dependency on newly emerging algorithm

reverted to old wellsorting algorithm

experimental inclusion of new wellsorting algorithm for code equations

do not drop arguments to 0, 1

Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.

Reintroduced nitpick_ind_intro attribute.
It looks like I need it nonetheless.

Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
This should now be all.

Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
these will be used by Nitpick, which will be released independently of Isabelle
2009, but they need to be in.

no base sort in class import

added HOL-Base image

moved value.ML to src/Tools

made repository layout more coherent with logical distribution structure; stripped some $Id$s

--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML

Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;

simproc for let

Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.

"arbitrary" merely abbreviates undefined

code identifier namings are no longer imperative

`code func` now just `code`

re-introduces axiom subst

polished code generator setup

discontinued special treatment of op = vs. eq_class.eq

Added setup for coherent logic prover.

generic value command

restructured and split code serializer module

tuned code generator setup

single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp

ML_Antiquote.value;

moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;

removed obsolete case_split_tac -- cannot work without;

eliminated obsolete case_split_thm -- use case_split;
added case_split_tac (works without context);
setup for induct_tacs.ML;

localized Least in Orderings.thy

eliminated theory CPure;

moved 'trivial classes' to foundation of code generator

different handling of eq class for nbe

constant HOL.eq now qualified

Sign.hide_const;

Generic conversion and tactic "atomize_elim" to convert elimination rules
to the object logic

postprocessing of equality

explicit class "eq" for operational equality

purely functional setup of claset/simpset/clasimpset;

pass imp_elim, swap to classical prover;

dropped superfluous code theorems

splitted class uminus from class minus

use random_word.ML earlier;

simplified infrastructure for code generator operational equality

replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);

interpretation of typedecls: instantiation to class type

tuned specifications of 'notation';

move itself into HOL types

global class syntax

added first version of user-space type system for class target

certificates for code generator case expressions

clarified declarations in class ord

moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;

proper syntax during class specification

moved Tools/integer.ML to Pure/General/integer.ML;

added lemma

final(?) iteration of sgn saga.

codegen.ML is now loaded in Pure again.

fixed codegen setup

ATP blacklisting is now in theory data, attribute noatp

updated code generator setup

new structure for code generator modules

new nbe implementation

simplified ResAtpset via NamedThmsFun;
proper simproc_setup for "neq", "let_simp";

using class target

simplified HOL bootstrap

replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;

use hologic.ML in basic HOL context;
tuned proofs;

CONVERSION tactical;

simplified keyword setup

added Theorem all_not_ex

tuned proofs: avoid implicit prems;

tuned boostrap

merged Code_Generator.thy into HOL.thy

moved IsaPlanner from Provers to Tools;

proper loading of ML files;

added a set of NNF normalization lemmas and nnf_conv

tuned

dropped HOL.ML

Isar definitions are now added explicitly to code theorem table

added class "default" and expansion axioms for undefined

explizit "type" superclass

TrueElim and notTrueElim tested and added as safe elim rules.

removed safe elim flag of trueElim and notFalseElim for testing.

added safe intro rules for removing "True" subgoals as well as "~ False" ones.

tuned ML setup;

dropped lemma duplicates in HOL.thy

tuned ML setup;
added @{claset};

removed legacy ML bindings;
simplified ML setup;
tuned declarations;

moved order arities for fun and bool to Fun/Orderings

updated (binder) syntax/notation;

tuned proofs;

prefer antiquotations over LaTeX macros;

typo in comment fixed

tuned

more robust syntax for definition/abbreviation/notation;

moved lemma eq_neq_eq_imp_neq to HOL

tuned hypsubst setup;

renamed 'const_syntax' to 'notation';

Sign.const_syntax_name;

simplified reasoning tools setup

added Equals_conv

moved HOL code generator setup to Code_Generator

lifted claset setup from ML to Isar level

cleaned up HOL bootstrap

cleanup basic HOL bootstrap

improved serialization for arbitrary

tuned;

proper const_syntax for uminus, abs;

renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes

added 'undefined' serializer

introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy

final syntax for some Isar code generator keywords

simplified code generator setup

tuned proofs;

- Added new "undefined" constant
- normalization_conv no longer expects term to
have form "Trueprop ..."

made evaluation_conv and normalization_conv visible.

removed the "tagging" feature

normalization uses refl now

new method "normalization"

slight adaption for code generator

quoted "if";

tuned concrete syntax -- abbreviation/const_syntax;

introduced characters for code generator; some improved code lemmas for some list functions

different object logic setup for CodegenTheorems

replaced syntax/translations by abbreviation;

adapted for definitional code generation

renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.

moved the "use" directive

Added setup for "atpset" (a rule set for ATPs).

improved codegen bootstrap

simplified Pure conjunction;

added theory of executable rational numbers

Added "evaluation" method and oracle.

added serialization for arbitrary

declare 'defn' rules;

removed problematic keyword 'atom'

setup: theory -> theory;

substantial improvements in code generator

declare the1_equality [elim?];

prefer ex1I over ex_ex1I in single-step reasoning;

simplified EqSubst setup;

tuned EqSubst setup;

removed obsolete cla_dist_concl;

provide cla_dist_concl;

removed obsolete induct_atomize_old;

structure ProjectRule;
updated auxiliary facts for induct method;
tuned proofs;

alternative iff syntax for equality on booleans, with print_mode 'iff';

eq_codegen now ensures that code for bool type is generated.

renamed rules to iprover

added code generator setup (from Main.thy);

the experimental tagging system, and the usual tidying

axclass: name space prefix is now "c_class" instead of just "c";

simp_implies: proper named infix;

Turned simp_implies into binary operator.

added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.)
renamed simplification rules for abs (abs_of_pos, etc.)
renamed rules for multiplication and signs (mult_pos_pos, etc.)
moved lemmas involving fractions from NatSimprocs.thy
added setsum_mono3 to FiniteSet.thy
added simplification rules for powers to Parity.thy

Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
of premises of congruence rules.

Constant "If" is now local

migrated theory headers to new format

tuned;

Simplifier already setup in Pure;

superceded by Pure.thy and CPure.thy;

new meta-level rules

arg_cong2 by Norbert Voelker

Move towards standard functions.

Moved oderings from HOL into the new Orderings.thy

the new subst tactic, by Lucas Dixon

added simproc for Let

removal of HOL_Lemmas

proof of subst by S Merz

Fixed print translation for ALL x > y etc

added ALL print-translation for > and >=.

Added "ALL x > y" and relatives.

Added > and >= sugar

removed a "clone" (duplicate code)

Added antisymmetry simproc

import -> imports

New theory header syntax.

New transitivity reasoners for transitivity only and quasi orders.

conversion of Hyperreal/MacLaurin_lemmas to Isar script

Merged in license change from Isabelle2004

removed obsolete sort 'logic';

new atomize theorem

_index1: accomodate improved indexed syntax;

simplified ML code for setsubgoaler;

use more symbols in HTML output

Added documentation for transitivity solver setup.

new material from Avigad, and simplified treatment of division by 0

Efficient, graph-based reasoner for linear and partial orders.
+ Setup as solver in the HOL simplifier.

replacing HOL/Real/PRat, PNat by the rational number development
of Markus Wenzel

* Support for raw latex output in control symbols: \<^raw...>
* Symbols may only start with one backslash: \<...>. \\<...> is no longer
accepted by the scanner.
- Adapted some Isar-theories to fit to this policy

print translation for ALL x <= n. P x

more general lemmas for Ring_and_Field

Tuned proof of choice_eq.

Added support for making constants final, that is, ensuring that no
definition can be given later (useful for constants whose behaviour is
fixed axiomatically rather than definitionally).

misc tidying

some basic new lemmas

removed some problems with print translations

added print translations tha avoid eta contraction for important binders.

*** empty log message ***

Added choice_eq.

Fixed problem with induct_conj_curry: variable C should have type prop.

modified induct method

order_less_irrefl: [simp] -> [iff]

removal of blast.overloaded

special syntax for index "1" (plain numeral hidden by "1" symbol in HOL);

added mk_left_commute to HOL.thy and used it "everywhere"

simplified locale predicates;

predicate defs via locales;

clarified syntax of ``long'' statements: fixes/assumes/shows;

tuned;

"_not_equal" dummy constant;

tuned ``syntax (output)'';

Replaced several occurrences of "blast" by "rules".

tuned declarations (rules, sym, etc.);

setup "rules" method;

renamed class "term" to "type" (actually "HOL.type");

converted simp lemmas;

tuned;

induct method: localize rews for rule;

lemmas induct_atomize = atomize_conj ...;
val local_imp_def = thm "induct_implies_def";

eliminated old "symbols" syntax, use "xsymbols" instead;

tuned;

removed obsolete (rule equal_intr_rule);

renamed inductive_XXX to induct_XXX;
added induct_impliesI;