tuned

Handle Subscript exception when looking up bound variables.

Added well-formedness check to Abst case in function prf_of.

added omission

bugfixes concerning strange theorems

fixed typo

const antiquotation clarified

clarified

handling of notation in class target

fixed document preparation

improved website integration

adjusted

split library index into templates

split library index into templates

structured

tidied version

simplified proof

continued localization

fixed typo

added nbe

test_proof: do not change Proofterm.proofs here (not thread-safe);

improved notion of 'nicer' fact names (observe some name space properties);

export is_hidden;

added bool_ord;

qualified Proofterm.proofs;

fun/function: generate case names for induction rules

append/member: more light-weight way to declare authentic syntax; tuned proofs;

made SML/NJ happy;

safe_exit: controlled_execution;

better compute oracle

better compute oracle

adapted Compute...

use "fun" for definition of "member" -> authentic syntax

ASCIIfied README

added list comprehension syntax

locale_const: in_class workaround prevents additional locale version of class consts;

notation: associate syntax to checked-unchecked term;

export class_prefix; removed obsolete const hiding;

tuned

changed order of class parameters

dropped square syntax

localized monotonicity; tuned syntax

dropped "brown" syntax

replaced Secure.evaluate by ML_Context.evaluate;

asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;

proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;

print the defined constants when finished; tuned

adjusted

tuned

added NEWS entry for function package

added hint for algebra

moved primitive operations to class.ML

fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.

dropped redundancy

various localizations

made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);

tuned

clarified implementation

propagation through class hierarchy

added function for evaluation by compiler invocation

more computation with rationals

localized further

continued

tuned

THIS_IS_ISABELLE_MAKEBIN;

updated;

README for polyml-5.1 binary distribution;

avoid very slow metis invocation (saves 1min on 1.60 GHz machine);

separate RecordPackage.timing flag;

tuned;

tuned file names etc.;

*** empty log message ***

added HOL-Statespace session;

be explicit about .ML files;

fixed HOL-Statespace for case-sensitive file-system;

tuned comments;

added Statespace library

tuned

fun command: use "reinit" between "function" and "termination"

parse_term: invoke full Syntax.check_term, not just standard_infer_types;

fixed typo

added subclass_rule

example with rational numbers

dropped superfluous inlining rule

tuned

went back to >0

changed back from ~=0 to >0

updated;

added XCONST syntax (keeps original spelling of const);

translations: use XCONST for input patterns (keeps original spelling of const);

random tidying of proofs

empty files are back -- referenced in Makefile;

dropped code redundancy

tuned

tuned proof

partially localized

continued

tuned;

fixed proof: no one_is_Suc_zero;

tuned Nominal entry;

clarified Haskell qualification heuristics

tuned abbreviations in class context

dropped superfluous inlining lemmas

removed empty files;

abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);

added @{sort}, @{type_syntax} antiquotations;

>0 -> ~=0

More changes from >0 to ~=0::nat

tuned

further comments

polished the proofs and added a version of the weakening lemma that does not use the variable convention

fixed proof: neq0_conv;

modernized specifications ('definition', 'axiomatization');

Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.

context_const_ast_tr: proper const_syntax_name (cf. @{const_syntax});

removed obsolete ML bindings;

modernized specifications ('definition', 'abbreviation', 'notation');

avoid very slow metis invocation;

misc tuning;

Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR