fixed codegen setup

added evaluation examples

main: wait_timeout (1 second);

tuned comments;

added sendback;

combining the relevance filter with res_atp

combining the relevance filter with res_atp

ATP blacklisting is now in theory data, attribute noatp

added Code_Setup

fixed OCaml bug

tuned

extended

added Eval_Witness theory

updated code generator setup

updated

renamed standard_read_XXX to standard_parse_XXX; added global_read/parse_XXX;

added implicit type mode (cf. Type.mode); added inner syntax parsers for sort/typ (no term/prop yet); infer_types: exception TYPE => error; read_vars: Syntax.parse_typ;

Syntax.global_read_sort;

infer_types: depend on Type.mode;

type mode: models certification mode (default, syntax, abbrev); replaced certify_typ_syntax/abbrev by certify_typ_mode;

replaced certify_typ_syntax/abbrev by certify_typ_mode; removed obsolete read_sort', read_typ', read_typ_syntax', read_typ_abbrev';

tuned order;

avoid low-level tsig;

fixed dummyT (used as constraint);

remove redundant assumption from Rep_range lemma

minimize imports

rename lemmas finite->finite_UNIV, finite_set->finite; declare finite[simp]

extended linear arith capabilities with code by Amine

fix the generation of eqvt lemma of equality form from the imp form when the relation is equality

moved Tools/xml.ML to General/xml.ML (again);

added generic wrapper for parse/read functions; renamed read_term to standard_read_term etc.;

tuned;

PrimitiveDefs.dest/abs_def;

PrimitiveDefs.dest_def; Syntax.standard_read;

Primitive definition forms.

moved support for primitive defs to primitive_defs.ML;

use logic.ML earlier; added primitive_defs.ML;

moved Tools/xml.ML to General/xml.ML (again); added primitive_defs.ML;

PrimitiveDefs.mk_defpair;

be a bit more ressource cautious with multi-threading (-M 20 instead of 99)

fixed syntax

simplified

fixed OCaml bug

*** empty log message ***

renamed keyword "to" to "module_name"

dropped code_axioms

moved appl syntax to PureThy; structure Lexicon: not hidden;

Lexicon.tokenize: do not appen EndToken yet; term: include var, &&;

Lexicon.tokenize: do not appen EndToken yet;

Lexicon.read_indexname/nat/variable;

moved appl syntax to PureThy; SimpleSyntax.read_typ/term/prop;

moved appl syntax to PureThy;

SimpleSyntax.read_prop;

added atbroy9

multi-threading with poly 5.1 test

new attribute [rotated]

tuned comments;

Simple syntax for types and terms --- for bootstrapping Pure.

added Syntax/simple_syntax.ML;

* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;

read_def_terms': restrict scope of disambiguation to individual term;

stream source: non-critical, assuming exclusive ownership;

added type constraints to resolve syntax ambiguities;

made SML/NJ happy;

schedule_tasks: alphabetical order for equivalent tasks;

simultaneous use_thys;

tuned ML bindings;

tuned

dropped code generator setup garbage

syntax fix

corrected code generator module names

new structure for code generator modules

code generator setup improved

adjusted

new structure for code generator modules

ClassPackage renamed to Class

updated

simultaneous use_thys;

removal of some refs

(un)interruptible: pass-through original thread attributes;

tuned; added jEdit mode spec;

HOL_USEDIR_OPTIONS: default to -M 1 (more robust);

added jEdit mode spec; tuned comments;

* Experimental support for multithreading, using Poly/ML 5.1;

schedule: misc cleanup, more precise task model;

schedule: more precise task model; improved error handling: first failure causes interrupt of all threads; misc cleanup;

schedule: more precise task model; removed obsolete structure Task;

fixed DESCRIPTION: single line; proper quoting of shell variables;

updated;

adapted ThyLoad.check_thy;

dropped

explizit checking for pattern discipline

proper handling of empty datatypes

improved class target: now considers class intro rules

new access interface in defs.ML

adaptions for code generation

proper implementation of rational numbers

localized of_nat

tuned

re-eliminated Option.thy

updated

PGIP change: thyname is optional in opentheory, markup even in case of header parse failure

Typo in comment

discontinued attached ML files; end_theory: fail on unresolved dependencies;

simplified ThyLoad.deps_thy etc.: discontinued attached ML files;

load_thy: try_ml_file unconditionally;

* Theory loader: old-style ML proof scripts are considered a legacy feature;

check_deps: really do reload the master text if required; load_thy: more robust check of corrupted deps; require_thy: outdate_thy if required; tuned;

Useful abbreviation of isatool commands used by Eclipse

thread-safeness: when creating certified items, perform Theory.check_thy *last*; tuned datatype proof;

Code to undo the function ascii_of

Fixing the code to undo the function ascii_of