added NEWS entry

added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation

merged

generalize type of is_interval to class euclidean_space

section -> subsection

generalize some lemmas about derivatives

uniqueness of Frechet derivative

implode pseudo utf8, i.e. decode byte-stuffed low ASCII characters;

merged

even more fun with primrec

refactored reference operations

tuned

tuned empty heap

merged

merged

Unification (flexflex) bug fix; making "auto" deterministic

moved "open" operations from Heap.thy to Array.thy and Ref.thy

only definite assignment

moved special operation array_ran here

remove primitive operation Heap.array in favour of Heap.array_of_list

tuned proof

tuned

Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;

specific ML_val vs. ML_command;

async_state: report within proper transaction context;

merged

simplified representation of monad type

attempt to reconstruct missing HOL/Codegenerator_Test/ROOT.ML;

merged

updated document

dropped passed irregular names

adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"

remove needless signature entry

references to ghc and ocaml

explicit code_datatype declaration prevents multiple instantiations later on

refrain from using datatype declaration -- opens chance for quickcheck later on

tuned proof

reverted to verion from fc27be4c6b1c

traceback for error messages

accomodate for different behvaiour of nitpick (c.f. also 180e80b4eac1)

introduced distinct session HOL-Codegenerator_Test

tuned bootstrap files

remove codegeneration-related theories from big library theory

drop unconvenient code declarations

build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test

general Future.report -- also for Toplevel.async_state;

simplified Isabelle_Process.Result: use markup directly;

run_command: actually observe "print" flag;

Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);

more precise timing;

more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations; misc tuning;

standard argument order; tuned;

do not open auxiliary ML structures; misc tuning;

tuned white space;

fixed spelling

merged

"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect

"prod" and "sum" replace "*" and "+" respectively

qualified constants Set.member and Set.Collect

"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect

merged

convert theorem path_connected_sphere to euclidean_space class

generalize more lemmas from ordered_euclidean_space to euclidean_space

avoid Old_Number_Theory; more precise dependencies;

misc tuning and modernization;

merged

once more a try with mkdir_leaf

refined semantics of mkdir_leaf: do not fail if directory already exists

avoid bitstrings in generated code

Updated NEWS

Add theory for indicator function.

Instantiate product type as euclidean space.

merged

repaired line ending

revert to plain for now mkdir

one unified Word theory

more speaking names

more speaking names

moved specific operations here

more speaking theory names

more speaking theory names

use existing bit type from theory Bit

split off Cardinality from Numeral_Type

added literal and typerep instances

mkdir_leaf -- avoiding surprises with typos in user-given paths

generalize some lemmas about derivatives

add lemma at_within_interior

generalize more euclidean_space lemmas

minimize dependencies on Numeral_Type

change type of 'dimension' to 'a itself => nat

generalize some euclidean_space lemmas

merged

rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly

rename functions

merged

unfold_fun_n

pervasive tuning of code

explicit printing function for applify

fail with low-level exception, not user error;

eliminated some unused bindings;

recovered some indentation from the depths of time;

cleaned by using descending instead of lifting

merged

move function

compile

compile

more elegant cheating

Sledgehammer can save some msecs by cheating

more precise error message for remote ATPs

move blacklisting completely out of the clausifier; the only reason it was in the clausifier as well was the Skolem cache

rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems

move "nice names" from Metis to TPTP format

move functions not needed by Metis out of "Metis_Clauses"

no setup is necessary anymore

adapt call

remove obsolete component of CNF clause tuple (and reorder it)

killed "expand_defs_tac"; it has no raison d'etre now that Skolemization is always done "inline"; the comment in the code suggested that it was used for other things as well but the code clearly did nothing if no Skolem "Frees" were in the problem

get rid of Skolem cache by performing CNF-conversion after fact selection

always perform "inline" skolemization, polymorphism or not, Skolem cache or not

always perform relevance filtering on original formulas