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;