renamed T.source_of' to T.source_position_of;

output_markup: check Markup.is_none;

added is_none; added inner_comment;

Args.name_source(_position) for proper position information;

[source=false] for quoted antiquotation avoids quote-escapes in output;

report antiquotations;

tuned;

report ML_source;

renamed P.ml_source to P.ML_source;

report doc_source;

added ML_source, doc_source;

antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;

added source_of';

P.doc_source and P.ml_sorce for proper SymbolPos.text;

oracle, header/local_theory/proof_markup: pass SymbolPos.text;

use SymbolPos.T list directly, instead of encoded SymbolPos.text;

ML_Context.add_antiq: pass position; @{lemma}: set source position;

ML_Context.add_antiq: pass position;

retrieve_thms: transfer fact position to result; tuned;

moved basic thm operations from structure PureThy to Thm; added position operations; tuned;

moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);

made SML/NJ happy;

removed obsolete present_html -- now part of regular theory presentation;

removed obsolete verbatim_source, results, chapter, section etc.; removed obsolete results, theorems(s); moved theorem result hook to proof_display.ML;

removed obsolete verbatim_source, results, chapter, section etc.; removed redundant end_index, end_theory;

ProofDisplay.add_hook;

simplified present_local_theory/proof;

ProofDisplay.theory_results;

removed obsolete present_results; added theory_results, which is subject to hooks (formerly in present.ML);

scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);

load_thy: no untabify (preserve position information!), present spans instead of verbatim source;

simplified markup commands;

simplified markup commands -- removed obsolete Present.results, always check text;

added untabify_content;

tuned;

removed obsolete untabify (superceded by SymbolPos.tabify_content);

tuned document;

removed obsolete theorems; handle generic XML markup as well (plain <markup> instead of <... class=markup>); misc tuning/update according to Pure/Generic/markup.ML;

Changed proof of strong induction rule to avoid infinite loop when premises of introduction rules contain equations.

token_kind_markup: complete coverage;

OuterSyntax.scan: pass position;

message: ignored if body empty;

load_thy: removed obsolete dir argument;

abstract type span, tuned interfaces; added report_token, report_span; markup ident tokens;

adapted ThyEdit operations;

added ignored, malformed transitions;

Symbol.source/OuterLex.source: more explicit do_recover argument; scan: pass position; removed obsolete prepare_command (now inlined in isar_syn.ML); renamed prepare_command_failsafe to prepare_command, reports tokens; load_thy: now based on ThyEdit operations, reports tokens and spans; tuned;

Isabelle.command: inline former OuterSyntax.prepare_command; Isar.command: based on fail-safe OuterSyntax.prepare_command;

load thy_edit.ML before outer_syntax.ML;

renamed unknown_span to malformed_span; added ident; tuned;

Symbol.source/OuterLex.source: more explicit do_recover argument;

updated generated file;

rudimentary code setup for set operations

<applet>: more XHTML 1.0 Transitional conformance;

Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;

<pre>: removed xml:space, is already default; result(s): avoid improper nesting of <pre> within <p>;

produce XHTML 1.0 Transitional; tuned charset name; renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);

renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);

Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!

changed code setup

re-arranged class dense_linear_order

rudimentary code setup for set operations

moved class wellorder to theory Orderings

added parse_token (from proof_context.ML);

read_tyname/const/const_proper: report position; moved parse_token to syntax.ML; tuned;

pass position to get_fact; tuned;

pass token source to typ/term etc.;

added name property operation; added local_fact; renamed proposition to prop (again);

renamed ML_Lex.val_of to content_of;

unified Args.T with OuterLex.token, renamed some operations; moved thm_sel to attrib.ML;

unified Args.T with OuterLex.token; RESET_VALUE of primitive parsers; export keyword_with; renamed keyword_sid to keyword_ident_or_symbolic; added int (from args.ML); added enum(1)', and_list(1)' (formerly in args.ML); removed obsolete arguments/generic_args1 (cf. parse/parse1 in args.ML);

unified Args.T with OuterLex.token; renamed val_of to content_of; added InternalValue kind; added datatype value/slot with static binding (from args.ML); renamed is_sid to ident_or_symbolic;

unified Args.T with OuterLex.token, renamed some operations; removed obsolete parse_args (cf. parse);

unified Args.T with OuterLex.token, renamed some operations; unified version of thm_sel (formerly in args.ML and spec_parse.ML);

unified Args.T with OuterLex.token; moved datatype value/slot and basic operations to outer_lex.ML; removed unused terminator; removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML); removed obsolete thm_sel (cf. attrib.ML); one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);

load args.ML later (after outer_parse.ML);

unified Args.T with OuterLex.token, renamed some operations;

read_asts: report literal tokens;

tuned error message;

pos_of_token: Position.T; removed unused display_token; tuned;

dest: sort strings; report: Output.status;

added literal;

read_token: more robust handling of empty text;

datatype token: maintain range, tuned representation; moved eof, stopper to lexicon.ML;

datatype token: maintain range, tuned representation; tuned messages;

datatype token: maintain range, tuned representation; added eof, stopper (from simple_parse.ML); str_of_token: no special case for EOF; misc tuning;

tuned SymbolPos interface;

YXML.parse: allow text without markup, potentially empty;

added content; simplified implode: interface and permissive padding via Position.distance_of; added range; renamed implode_delim to implode_range;

added distance_of (permissive version); added no_range; tuned;

count offset as well; more uniform treatment of invalid fields; tuned;

added offset/end_offset;

tuned formatting;

clean up dead code

made SML/NJ happy;

FundefLib.try_proof : attempt a proof and see if it works

added lemmas

inner_syntax markup is back;

disabled inner_syntax markup for now;

added read_token -- with optional YXML encoding of position; tuned parse operations: print position instead of echoing input (now encoded!); do not export obsolete read operation;

parse_token: use Syntax.read_token, pass full position information;

tuned;

map_default: more explicit scope;

datatype lexicon: alternative representation using nested Symtab.table;

simplified Antiquote signature;

more precise positions due to SymbolsPos.implode_delim; added source' for SymbolPos.T;

simplified Antiq: regular SymbolPos.text with position; renamed read_arguments to read_antiq; tuned;

renamed SymbolPos.scan_position to SymbolPos.scan_pos; implode/explode: explicit type text = string; added implode_delim; explode: Position.reset_range;

only increment column if valid; more robust handling of invalid entries; clarified line/line_file: no column here; added start = (1, 1); added reset_range; tuned;

install_pp Position.T;

Position.start;

SymbolPos.explode;

improved position handling due to SymbolPos.T;

improved position handling due to SymbolPos.T; SymbolPos.scan_comment; tuned;

Antiquote.read/read_arguments;

updated type of nested sources;

improved position handling due to SymbolPos.T; SymbolPos.scan_comment_body; tuned;

adapted Scan.extend_lexicon/merge_lexicons;

renamed scan_antiquotes to read; renamed scan_arguments to read_arguments; improved position handling due to SymbolPos.T; tuned;

export not_eof;

reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;

advance: single argument (again); added range; tuned;

Symbols with explicit position information.

added General/symbol_pos.ML;

Interpretation command (theory/proof context) no longer simplifies goal.

added lemma

made SML/NJ happy;

Reverted last change, since it caused incompatibilities.

fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);

T.end_position_of; tuned;

adapted Antiq;

parse_sort/typ/term/prop: report markup;

sort/typ/term/prop: inner_syntax markup encodes original source position; added typ/term/prop_group (without inner_syntax markup);

removed obsolete range_of (already included in position); added end_position_of; replaced scan_string by scan_quoted (which keeps quotes and includes alt_string as well); misc tuning;

report markup;

Antiq: inner vs. outer position; scan_antiq: use T.scan_quoted;

of_properties: observe Markup.position_properties';

added position_properties'; renamed prop to proposition; added attribute, method;

token: maintain of source, which retains original position information; removed count/counted, advance position via scanned source;

moved OuterLex.count here;

improved recover: also resync on symbol/comment/verbatim delimiters;

advance: operate on symbol list (less overhead);

added token;

fix HOL/ex/LexOrds.thy; add to regression

added report;

removed axiom; added fact, dynamic_fact, prop;

get_fact: report position;

Facts.lookup: return static/dynamic status;

position scanner: encode token range;

added encode_range; tuned;

added end_line, end_column properties;

meta_subst: xsymbols make it work with clean Pure;

abstract type Scan.stopper, position taken from last input token;

abstract type Scan.stopper;

abstract type stopper, may depend on final input;

removed obsolete apply_theorems(_i);

tuned signature; eliminated obsolete pervasives;

removed obsolete note_thms_cmd;

simplified defer_recdef(_i): plain facts via Attrib.eval_thms;

tuned description;

replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/

Quoted terms in consts_code declarations are now preprocessed as well.

Exported eval_wrapper.

- corrected bogus comment for function inst_conj_all - tuned function obtain_fresh_name

removed dead code

simplified prepare_command;

Isar.command: explicitly set transaction position, as required for prepare_command errors; adapted Isabelle.command;

Updated locale tests.

Generalised polynomial lemmas from cring to ring.

Removed import and lparams from locale record.

made setsum executable on int.

Tuned (for the sake of a meaningless log entry).

New locales for orders and lattices where the equivalence relation is not restricted to equality.

added hint about writing "x : set xs".

simple lifters

dropped imperative monad bind

facts_of

improved morphism

SML_imp, OCaml_imp

clarified

tuned

Zorn's Lemma for partial orders.

Definitions and some lemmas for reflexive orderings.

Lemmas added

New theory on divisibility.

Renamed theorems; New theory on divisibility.

New theorems on summation.

Unit_inv_l, Unit_inv_r made [simp].

New theory on divisibility; Restructured presentation.

Unit_inv_l, Unit_inv_r made [simp]; Renamed theorems; New theory on divisibility.

Haskell now living in the RealWorld

corrected Pure dependency

added removeAll

tuned; explicit export of element accessors

PureThy: dropped note_thmss_qualified, dropped _i suffix

some steps towards explicit class target for canonical interpretation

declare

*** empty log message ***

simplified a proof

tuned function name

tuned bootstrap order

subclass now also works for subclasses with empty specificaton

dropped PureThy.note; added PureThy.add_thm

added class preorder

dropped locale (open)

added explicit root theory; some tuning

tuned

dropped locale (open)

(re-)added simp rules for (_ + _) div/mod _

(re-)added simp rules for (_ + _) div/mod _

added explicit purge_data

added code generation

fixed code generator setup

(adjusted)

Tuned and corrected ideal_tac for algebra.

Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy

Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy

Tuned and simplified proofs

Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra

Relevant rules added to algebra's context

renamed item to span, renamed contructors; added span_range;

adapted ThyEdit.span;

maintain token range;

tty loop: do not report status;

added type range;

renamed command span markup;

SideKickParsedData: minimal content;

(adjusted)

(adjusted)

added verification framework for the HeapMonad and quicksort as example for this framework

build jedit plugin only if jedit is available;

misc tuning;

more class instantiations

refined code generator setup for rational numbers; more simplification rules for rational numbers

moved op dvd to theory Ring_and_Field; generalized a couple of lemmas

fixed Scala path;

tuned build order;

proper purge_tmp; remove .cvsignore files;

tuned message;

tuned line breaks (NB: generated text is inserted here);

proper usage message; more precise perl replacements; less verbosity;

make Isabelle source distribution (via Mercurial);

explicit Distribution.changelog;

structure Distribution: swapped default for is_official;

ThyInfo.remove_thy;

structure Distribution: swapped default for is_official; removed obsolete (?) sync/sleep;

use ../isabelle.sty and ../isabellesym.sty;

tuned whitespace;

removed old checklist;

obsolete;

tuned;

discontinued maketags;

assume GNU tar and find; Admin/build all; discontinued maketags;

tuned;

use ../isabellesym.sty, which is always available;

Admin/build browser;

less verbosity;

Administrative build -- finish Isabelle source distribution.

simplified proofs

beautified proofs

added lemmas

Added Standardization theory to nominal examples.

Added Standardization theory.

editor model: run interactively for now;

updated generated file;

identify: more informative id in Toplevel.debug mode; interactive state transformations: dispose descendants *before* running next command, bypass for control commands; editor model: actually run affected commands; misc tuning;

shortlogentry/filelogentry: show shortdate and full description;

Removed uses of context element includes.

added Isar.command, Isar.insert, Isar.remove (editor model);

export type id with no_id and create_command; basic support for editor model: insert_command, remove_command; refined command status; misc tuning;

tuned;

renamed IsarCmd.nested_command to OuterSyntax.prepare_command;

load thy_edit.ML before isar.ML;

modernized specifications and proofs; tuned document;

Removed uses of context element includes.

tuned

tuned code theorem bookkeeping

tuned changelogentry;

refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);

support for command status;

added status channel; writeln_default: suppress empty messages;

added status channel;

tuned;

simplified commit_exit;

simplified commit_exit: operate on previous node of final state, include warning here; misc tuning;

removed obsolete commit_exit;

added command 'linear_undo'; tuned;

removed command 'redo'; added command 'linear_undo';

adapted ThyInfo.end_theory;

dropped map; fixed swap

curried gcd

cover macbroy as well; tuned;

tuned filelogentry;

print_mode "test_markup": do not change prompt, otherwise Proof General will not work;

tuned message;

updated generated file;

inform_file_processed: Isar.init_point last!

removed HOL-Complex, which has been discontinued after Isabelle2008;

added HOL-Nominal image;

removed obsolete Pure/General/history.ML;

inform_file_processed: try harder not to fail, ensure

commit_exit: proper error;

export EXCURSION_FAIL;

dropped junk

moved bootstrap of simplifier

tuned

end_theory: no result;

removed obsolete Toplevel.RESTART;

proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML); removed obsolete Toplevel.RESTART;

eliminated internal command history -- superceeded by global Isar state (cf. isar.ML); added commit_exit; removed obsolete exception RESTART; init_theory: removed obsolete kill argument; removed obsolete undo_limit, undo_exit, kill, history; misc tuning;

adapted IsarCmd.init_theory;

renamed theory to init_theory, removed obsolete kill argument; removed unused init_toplevel, begin_theory, end_theory; print_theorems: Toplevel.previous_node_of;

added commit_exit;

single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp

renamed conversions to _conv, tuned

Simplified proofs

Simple theorems about zgcd moved to GCD.thy

Theorem names as in IntPrimes.thy, also several theorems moved from there

Fixed proofs.

ProofNode.current

command 'redo' no longer available;

replaced obsolete ProofHistory by ProofNode (backtracking only);

removed obsolete 'redo' command; cannot_undo: global history; tuned;

removed obsolete history commands; moved back, cannot_undo to isar_syn.ML;

Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).

obsolete (cf. proof_node.ML);

removed Isar/proof_history.ML; added Isar/proof_node.ML

added further simple interfaces

simpsets as pre/postprocessors; generic preprocessor now named function transformators

unified curried gcd, lcm, zgcd, zlcm

Sorts.weaken: abstract argument; tuned;

Sorts.weaken: abstract argument;

instance real_field < field_char_0; instance star :: (field_char_0) field_char_0

re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef

Fract now total; improved code generator setup

simple inheritance concept

tuned thyname lookup

fixed layout

explicit completions of arities

tuned order

antiquotation

improved code generator setup

explicit dependency

class instead of axclass

tuned import

separate class dvd for divisibility predicate

temporarily disable at-sml-dev-p

updated generated file;

restart: Isar.init_point;

proper_inform_file_processed: Isar.init_point starts fresh command sequence;

activated new versions of undo, kill_proof;

activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;

added print;

added ProofGeneral.isar_kill_proof;

added Isar.init_point, Isar.kill;

export init_point; added kill, kill_proof; misc tuning;

added Isar.linear_undo;

tuned;

tty interaction: do not move point after error;

change_lexicons: no verbosity;

added Isar.undo, which emulates old-style undo on global tty state;

provide old-style undo operation (still unused); clarified command category; misc tuning;

added prompt markup;

@{lemma}: allow terminal method;

@{lemma}: allow terminal method, close derivation unless (open) mode is given;

added is_diag;

slightly improved @{lemma} (both for latex and ML); misc tuning;

misc tuning; more explicit error messages;

Fixed (harmless) typo in closing *}.

by intro_locales -> ..

instance real_field < field_char_0

remove redundant lemmas about cmod

removed owner;

tuned description;

changes wrt. gitweb style;

style = isabelle (based on gitweb);

rearrange instantiations

added get_first; tuned;

updated generated file;

updated generated file;

fix more typos

fix another typo

fix typo

updated generated file;

global commands: explicit graph; tuned;

export str_of;

clarified code

exported weaken combinator

refined arity property concept

fix: using IntInf.int for SML

moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy; non-pervasive touch_thy, remove_thy;

removed obsolete touch_child_thys; simplified touch_thy, remove_thy, kill_thy -- inlined;

moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy; removed unused touch_child_thys, touch_thy, remove_thy, kill_thy;

more qualified ThyInfo names;

begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear! replaced warning by error for non-existant theory/ML info;

removed unused href_opt_name; begin_theory: unconditional file links, proper output of parentheses;

migrated at-sml-dev-p to macbroy24, hoping for more reliable hardware

retired mac-sml-dev.

absolute imports of HOL/*.thy theories

prefer theorem names without numbers

HOL-NSA

added marginal setup for code generation

use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero

removed old NSPrimes, cf. NSA/Examples/;

cvsps: back to non-verbose mode;

removed old Complex/ex/NSPrimes.thy;

maxfiles = 50;

more sessions;

more precise dependencies for HOL-Word and HOL-NSA;

fixed extremely slow proof of Chain_inits_DiffI

add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)

move proofs of add_left_cancel and add_right_cancel into the correct locale

cvsps -v (verbose);

removed nonstandard analysis theories to HOL-NSA

moved theories to HOL/NSA

add HOL-NSA

use patched cvsps to workaround loss of "foo: bar;" log entries;

move nonstandard analysis theories to NSA directory

back to default style, which shows files in changelog view;

added description;

tuned;

logrotate setup;

redirect stderr as well;

output to log file;

specific to CVS; some updates for Java etc.;

Isabelle repository service.

ensure hg/.hg/hgrc;

hgrc for conversion and web service;

provide HGRCPATH, taken from cvs/Admin; replaced MERCURIAL by HG, which is also used by Mercurial internally;

code antiquotation roaring ahead

tuned

adjusted postprocessort setup

added lemma antiquotation

adjusted rep_datatype

Adapted to changes in perm_simp / swap_simps.

Replaced all but one occurrence of perm_simp_tac by perm_simproc_app, since perm_simp_tac now behaves in a different way (due to changes in swap_simps).

Rewrote code to use swap_simps rather than calc_atm (which tends to produce ridiculously large nested if-expressions).

moved HOL-Plain up;

rename Doc doc-src;

renamed Contents to Dirs to avoid case-conflict with doc/Contents;

section -> subsection

convert Isabelle CVS to Mercurial;

use begin and end for proofs in locales

exclude Distribution/bin/Isabelle;

init_theory: pass name explicitly; empty transition: empty name;

replaced datatype category constructivism by is_theory/is_proof;

Toplevel.init_theory: pass name explicitly;

command: always keep transition, not just as initial status; improved datatype category (moved here from outer_keyword.ML);

cached code for code antiquotation

code antiquotation roaring ahead

cleaned up some code generator configuration

tuned;

added datatype category;

replaced datatype kind by OuterKeyword.category;

clean: HOL-Plain;

prove lemma finite in context of finite class

added HOL-Plain;

explicit identification of toplevel commands, with status etc.; explicit point for tty mode; prompt: markup prev id; tuned signature;

added name_of; added get_id/put_id; tuned;

added get_id/put_id;

(removed Complex/ROOT.ML)

HOL += HOL-Complex

HOL += HOL-Complex

tuned

HOL += HOL-Complex

put file dependencies on separate lines

range_composition no longer in simp set

remove simp attribute from range_composition

rename INF to INFM

remove unused lemmas ub2ub_monofun' and dir2dir_monofun

remove redundant instance proof finite_po < cpo

remove unused lemma is_lub_Iup'

replace lub (range Y) with (LUB i. Y i)

add file dependencies

universal bifinite domain

isomorphisms between naturals and sums, products, and finite sets

theory of algebraic deflations

theory of eventually-constant sequences

rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM

rename compact_approx to compact_take

rename approx_pd to pd_take

split Completion.thy from CompactBasis.thy

filemap for CVS -> Mercurial conversion;

reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma

New theory of deflations and embedding-projection pairs

remove unused Cset.thy

added facts to lemma swap_simps and tuned lemma calc_atms

simplified retrieval of theory names of consts and types

tagged arities

HOL-Complex with proof terms

code generator setup for "int" also works under eta-contraction

added ML/ml_thms.ML;

tuned;

tuned;

additional ML antiquotations;

moved theorem values to ml_thms.ML;

Isar theorem values within ML.

added ML/ml_thms.ML;

updated generated file;

allow overlap of minor keywords and commands;

include HOL-Plain;

tuned args parser (cf. args.ML); tuned signature;

replaced simple_text by fully-featured parse_args;

tuned nested args parser; export generic_args1;

@{lemma}: 'by' keyword;

ML: improved antiquotations;

added macro interface; added @{let}, @{note};

tuned;

added thm_name, opt_thm_name;

adjusted import

adjusted import

added a lemma to at_swap_simps

remove cset theory; define ideal completions using typedef instead of cpodef

Args.theory;

added context/theory scanner;

Args.context;

fix: need to beta/eta normalize

established Plain theory and image

added dummy citiation

dropped recdef

class theory name lookup improved

modernized specifications;

tuned proofs;

modernized specifications;

modernized specifications;

typo

re-use official outer keywords;

scan: prefer command over keyword, allowing lexicons to overlap;

moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces; lexicons: allow overlapping keywords/commands -- warning instead of error;

moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces; moved check_text here;

antiquote: need to quote outer keywords;

tuned;

moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;

- Equivariance simpset used in proofs of strong induction and inversion rules now contains perm_simproc_app and perm_simproc_fun as well - first_order_matchs now eta-contracts terms before matching - Rewrote code for proving strong inversion rule to avoid failure when one of the arguments of the inductive predicate has an atom type

pprint: back to proper output of markup, with workaround for Poly/ML crash;

back to 1.36 (Poly/ML crash!?);

updated generated file;

YXML: no special treatment of white space;

pprint: proper output of markup (important for token translation);

ml_code_antiq: proper scanner combinators; ML_Antiquote.value;

moved concrete antiquotations to ml_antiquote.ML;

Antiquote.Open/Close;

add_antiq: more general notion of ML antiquotation; eval_antiquotes: support blocks and background context; moved concrete antiquotations to ml_antiquote.ML;

added Open/Close -- checked blocks;

added pprint_thy_ref;

Common ML antiquotations.

added ML/ml_antiquote.ML;

ML_Antiquote.value;

added isaantiqopen/close;

Logic.all/mk_equals/mk_implies; Term.all;

moved implies to logic.ML; removed equals; qualified all;

added all, is_all; improved dest_all; added implies (from term.ML);

Logic.implies;

Logic.is_all;

Term.all;

Logic.all/mk_equals/mk_implies;

session name: empty for Pure and by default;

induct_tac: allow omission of arguments;

info: default name is "", not "Pure";

moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;

removed obsolete dest_concls;

induct_tac: mutual rules work as for method "induct";

tuned get_inductT: *all* rules for missing instantiation; exported get_inductT;

induct_tac: infer mutual rule from types, as for proper induct method;

induct_tac/case_tac: nested tuples are split as expected;

induct_tac: old conjunctive rules no longer supported;

updated generated file;

induct_tac: rule is inferred from types;

cleaned up some proofs; removed unused stuff about totally-ordered sets; import Main

use new-style abbreviation/notation for fix syntax

import_export_proof: simplified thm definition -- PureThy.name_thm does the job;

added query_type/const/class (meta data);

the_tags: explicit error message; new_decl: Position.thread_data;

activate_context: strict the_context, no fallback on theory context;

remove unused constant liftpair

simplify profinite class axioms

clean up and rename some profinite lemmas

move at-sml-dev-e to macbroy23

replace SetPcpo.thy with Cset.thy

updated for 2008; proper name of TUM;

(removed non-present change)

explicit thm context for error messages

using tages to find theory names

type constructors now with markup

fixed bind error for malformed primrec specifications

DatatypeProp.make_distincts: only one half of each symmetric pair is constructed

streamlined definitions

moved Float.thy to Library

removed SetPcpo.thy and cpo instance for type bool; added Cset.thy with pcpo type 'a cset isomorphic to 'a set; updated ideal completion theory to use cset

moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale

add lemma Abs_image

added some lemmas; reorganized into sections; tuned proofs

added some lemmas; tuned proofs

tuned

replace less_lift with flat_less_iff

tweak lemmas adm_all and adm_ball

move lemmas into locales; restructure some proofs

add lemmas take_chain_less and take_chain_le

disposed Sign.read_typ etc;

renamed is_abbrev_mode to abbrev_mode; added private get_sort (from sign.ML);

ProofContext.abbrev_mode;

moved get_sort to Isar/proof_context.ML; removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;

tuned signature; removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);

private add_used (from drule.ML); Variable.declare_names;

Variable.declare_typ;

added declare_typ;

moved add_used to Isar/rule_insts.ML;

export read_typ/cert_typ -- version with regular context operations; tuned;

export read_typ/cert_typ -- version with regular context operations;

tuned signature; removed duplicate of RecordPackage.read_typ; replaced Typetab by existing Typtab;

removed duplicate of DatatypePackage.read_typ;

add lemma cfcomp_LAM

add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);

slightly tuned

generalized induct_scheme method to prove conditional induction schemes.

add lemma iterate_iterate

* Disposed old term read functions;

replace preorder class with locale

add lemma compact_imp_principal to locale ideal_completion

added type_constraint (formerly in type_infer.ML, which is now loaded later);

TypeExt.type_constraint;

simplified TypeInfer.infer_types;

improved error output -- variant/mark bounds; simplified infer_types -- always freeze, no result substitution;

load type_infer.ML after Syntax module;

eliminated old Sign.read_term/Thm.read_cterm etc.;

moved ProofContext.pretty_proof to ProofSyntax.pretty_proof; read_term: imitate old behaviour (allow_dummies, mode_schematic);

export transfer_syntax; added allow_dummies feature (for legacy emulations); moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;

removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);

added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);

removed obsolete read_def_cterms/read_cterm;

load proof term operations later;

more antiquotations;

OldGoals.read_prop;

OldGoals.simple_read_term;

simplified Abel_Cancel setup;

updated generated file;

pervasive cut_inst_tac;

added a progress lemma and tuned some comments

* Rules and tactics that read instantiations now demand a proper context;

added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML); pervasive operations; tuned;

renamed rename_params_tac to rename_tac;

removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML); removed obsolete rename_tac, rename_last_tac; renamed rename_params_tac to rename_tac;

removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm; removed obsolete abbreviations for ML tactic scripts;

removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);

inst1_tac: proper context;

pervasive RuleInsts;

updated generated file;

converted ML proofs;

added read_instantiate;

ML tactic: do not abstract over context again;

export eof;

removed obsolete inst;

atomize: proper context; RuleInsts.read_instantiate;

atomize: proper context;

RuleInsts.read_instantiate;

ptac/prolog_tac: proper context;

allE_Nil: only one copy, proven in regular theory source;

deriv_tac/DERIV_tac: proper context;

sum3_instantiate: proper context;

eliminated OldGoals.inst;

updated generated file;

method "tactic": only "facts" as bound value; added method "raw_tactic";

Export a wrapper for all semiring_normalizers

proper context for tactics derived from res_inst_tac;

added ~: and ~=; fixed SOME, which is now \<some> not \<epsilon>;

export subgoal_tac, subgoals_tac, thin_tac;

prove: full Variable.declare_term, including constraints;

prove_standard: more precises argument passing; proper context for tactics derived from res_inst_tac;

InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;

simplified InductTacs.case_tac/induct_tac;

tuned proof;

removed obsolete nat_induct_tac -- cannot work without;

removed obsolete case_split_tac -- cannot work without;

removed unused excluded_middle_tac; proper context for tactics derived from res_inst_tac; tuned setup;

updated geenrated file;

qualified old res_inst_tac variants;

proper context for tactics derived from res_inst_tac;

updated generated file;

obsolete;

certify_term: reject qualified frees;

removed experimental Poplog/PML support; removed obsolete ML_SUFFIX; some reformatting;

removed obsolete ML_SUFFIX; some reformatting;

removed experimental Poplog/PML support;

removed obsolete ML_SUFFIX;

removed exotic 'token_translation' command;

proper name for LinearQuantifierElim;

removed old theorem database;

map_const: soft version, no failure here (recovers hiding of consts, because a hidden name is illegal and rejected later);

hide: delete all accesses from extra names -- reduces ambiguity in extern;

map_const: soft version, no failure here;

skolem_fact/thm: uniform numbering, even for singleton list; declare_skofuns: eliminated recovery via Clausify_failure -- should be sufficiently robust as is;

hide (open);

no_notation instead of hide;

* Recovered hiding of consts;

updated generated file;

back to CodeTarget.code_width;

hide -> hide (open)

use regular error function;

add lemma finite_image_approx; remove unnecessary sort annotations

change orientation of fix_eqI and convert to rule_format; add lemma fix_ind2

export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here);

removed obsolete skolem declarations -- done by Theory.at_end;

tuned setup;

remove unnecessary import of Ffun; add lemma admD2

imports Ffun

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context; eliminated obscure theory merge/transfer -- use explicit theory context instead;

ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;

sane versions of (qualified_)thms_of_thy;

Facts.dest/export_static: content difference; tuned;

dest/export_static: content difference; tuned comments;

declare_skofuns/skolem: canonical argument order; minor tuning;

Facts.dest/export_static: content difference;

correction

tuned

Removed hide swap

fixed type

lemma modified

typo

had to add rule: because induct_tac no longer works correctly

Hid swap

some reformatting;

added CK_Machine to the nominal section

soundness and completeness proofs for a CK machine as well as proofs for type preservation