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

metis

tuned ML setup;

fixed imports from ../../Auth;

turned Unify flags into configuration options (global only);

usedir: added options -M -T for multithreading;

removed 'declare' from tactic emulations;

theory loader: removed obsolete update_thy (coincides with use_thy); tuned; tuned comments;

theory loader: removed obsolete update_thy (coincides with use_thy);

theory loader: added use_thys, removed obsolete update_thy;

theory loader: added use_thys, removed obsolete update_thy; various global ML references of Pure and HOL have been turned into configuration options;

Issue a warning, when "function" encounters variables occuring in function position, as in "f (g x) = ..." where g is a variable.

more error handling

added more instances;

simplified internal interfaces; cong rules are now handled directly by "context_tree.ML"

split off Option theory

new nbe implementation

more robust simproces

tuned

simplified proofs

split off theory Option for benefit of code generator

changed import order

added more instances;

ML-Systems/overloading_smlnj.ML;

Overloading in SML/NJ.

Added renaming function to prevent correctness proof for realizer of induction rule to fail because of name clashes between parameters and predicate variables.

No document for Pretty_Int theory.

nbe improved

removed

simultaneous use_thys;

reactivated Nominal/Examples/Class.thy;

replaced outdated flag by update_time (multithreading-safe presentation order);

sort indexes according to symbolic update_time (multithreading-safe);

use separate trace flag instead of Output.debug;

named some CRITICAL sections;