tuned header

switched import from Main to List

switched import from Main to PreList

explicit import of theory ATP_Linkup

explicit import of theory Main

swtiched ATP_Linkup and PreList in theory hierarchy

ML_OPTIONS="-H 1500" -- potentially works around GC core dump;

added Id, some cleanup

tuned message;

renamed IsabelleResult to IsabelleProcess.Result;

Isabelle process wrapper for JVM platform (tentative implementation in Java, which is to be replaced by a sane source language eventually);

tuned messages;

Isar loop: recover after toplevel crashes;

secure_main: enforces terminator, to gain robustness;

text_of: make double sure that result is well-formed, to avoid recurrent failures;

ML_OPTIONS="-H 1000" -- potentially works around GC core dump;

added off-line parse; read: no recovery on non-interactive source, yields proper errors;

(alt)string: allow explicit character codes (as in ML);

added nested 'Isabelle.command';

updated;

special_end: replaced Z by dot;

output_prompt: CRITICAL;

declaration of instance parameter names

exported declare_names

new primrec

instantiation target rather than legacy instance

proper treatment of code theorems for primrec

dropped Instance.instantiate

Adding "ex/Induction_Scheme.thy" to tests

experimental version of automated induction scheme generator (cf. HOL/ex/Induction_Scheme.thy)

tuned further

renamed ML_PID to PID;

R&F: added sgn lemma Prefix: sledge-hammered

temporary code generator work arounds

fixed slip

-authentic primrec

dropped legacy bindings

authentic primrec

dropped void space

added new primrec package

load sum_tree.ML

factored out handling of sum types again

added test_markup; added channel markup and specials;

moved basic test_markup to isabelle_process.ML;

added channels; added markup operation, which operates on plain strings instead of raw output;

replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;

check persistent sessions;

tuned signature;

made SML/NJ happy;

removed -e flag from most sessions;

instance int,real :: lordered_ring

methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.

tuned class parts

dropped Classpackage.thy

tuned

added parser for multi_arity

added constrain_thm

canonical instantiation

map_product and fold_product

interface and distinct simproc tuned

improved

interpretation of typedefs

simplified infrastructure for code generator operational equality

added something about instantiation target

switch poly to 5.1, removed -e flag from most sessions

switch at-poly main to poly 5.1

make mac-poly non-experimental

make at64 non-experimental

Isabelle process wrapper -- interaction via external program.

Toplevel.loop: explicit argument for secure loop, no warning on quit;

added Isar.secure_main; pass Secure.is_secure to Toplevel.loop;

added Tools/isabelle_process.ML;

isabelle process: replaced option -p by -W (process wrapper);

replaced option -p by -W (process wrapper); tuned PGIP option setup;

\<chi> is now considered a letter; tuned;

symbol chi is also a letter;

improvements

overloading target

interface for unchecked definitions

shifted "fun" command to Wellfounded_Relations

updated

Eliminated unused theorems minusinf_ex and minusinf_bex

first working version of instance target

interpretation for typedefs

using intro_locales instead of unfold_locales if appropriate

more canonical attribute application

adjustions to due to instance target

new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.

*** empty log message ***

added {#.,.,...#}

tuned

stripped down

isabelle-process: option -p echos ISABELLE_PID;

commit: non-critical, otherwise session restart will result in deadlock!

instance command as rudimentary class target

dropped dead code

polyml: default heap size is back to -H 200 (people are still using machines with < 1GB of memory; no need to workaround heap problems of polyml-5.0 anymore);

an example file for how to treat Felleisen-Hieb-style contexts in nominal

removed (cf. object_logic.ML);

added base_sort; added typedecl, dependent on base_sort (cf. intermediate typedecl.ML and former sign.ML, HOL/Tools/typedef_package.ML); typedecl: recovered proper use of Syntax.type_name;

removed typedecl.ML (cf. object_logic.ML);

ObjectLogic.typedecl;

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

simplified using sledgehammer

Chained theorems are no longer mentioned in metis calls and (if used) they prevent the output of a structured proof.

comment

(reverted to unnamed infix)

simplified interpretations

deleted looping code theorem

to_set now applies collect_mem_simproc as well.

naming policy for instances

tuned interfaces of class module

dropped dead code

dropped legacy unnamed infix

dropped implicit assumption proof

dropped legacy ml bindings

tuned titles;

moved titles;

tuned title;

tuned titles;