Removed pointless backtracking from arith_tac

Improved error messages.

*** empty log message ***

tuned;

obsolete;

obsolete;

tuned;

\isasymindex made text mode;

isatools "symbolinput" and "nonascii" have disappeared;

added HOL-Library;

tuned;

updated;

removed altogether;

removed unused stuff;

Updated.

oops;

bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";

updated reserved words of HOL;

* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam" -- INCOMPATIBILITY;

obsolete;

removed additional blank line (confuses some versions of make);

obsolete;

- Changed type of invoke_codegen - Added combinators for sequences

- Added code generator interface for types - Changed type of invoke_codegen

Fixed bug in function find_paths.

Added example file for intuitionistic logic (taken from FOL).

Added support for code generation.

Recursive equations to be used for code generation are now registered via RecfunCodegen.add

Code generator for recursive functions.

Tuned header.

Code generator for datatypes.

Moved contents to files datatype_codegen.ML and recfun_codegen.ML

Turned subcls1 into an inductive relation to make it executable.

Example for code generator.

Added examples for code generator.

Added code generator setup.

Tuned code generator setup.

Added new files (code generator and examples).

Moved code generator setup from Recdef to Inductive.

Replaced several occurrences of "blast" by "rules".

document root;

tuned

HOLCF/IMP converted to Isar

HOL/IMP converted to Isar

converted to Isar

latex output setup

tuned for latex output

setup [trans] rules for calculational Isar reasoning

use /var/tmp (which happens to be more spacious on atbroy37);

new-style theory; proper declarations of various induction rules;

added Main.ML;

restart_loader: do *not* ThyLoad.reset_path;

tuned print_state interfaces;

optional PGML markup;

added writelns;

use "xml.ML";

export writeln_default; tuned prefix_lines;

tuned print_goals interfaces;

added General/xml.ML;

Basic support for XML output.

Slightly generalized the agents' knowledge theorems

added default_type;

tuned line breaks in HTML source;

fixed dest atts;

refrain from peeking at tags;

include session graph;

replaced record_split by the cases method

intro and elim now require arguments

record extend and truncate exercises

use Main;

* Pure/obtain: "thesis" now internal (use ?thesis); * Pure: generic 'sym' / 'symmetric' attributes; * Provers/classical: 'swapped' attribute; * HOL: proper rules less_induct and wf_induct_rule;

Syntax.internal thesis;

tuned xtra_netpair;

clarified sym_del;

added 'swapped' attribute; tuned xtra_netpair; tuned;

added the_mk_cases;

tuned;

renamed Finite to Finite_Set;

less_induct, wf_induct_rule;

renamed theory Finite to Finite_Set and converted;

this material already part of HOL/Set.thy;

sym [sym];

tuned;

iff;

updated;

adapted intr/elim uses;

eliminated old use of intro/elim method; tuned;

simplified proof (no longer use swapped rules);

fixed intro steps;

tuned declarations (rules, sym, etc.);

removed unused functionality (weight etc.);

simple version of 'intro' and 'elim' method; use ContextRules.find_rules;

added 'print_rules' command;

added print_rules;

simplified NetRules;

export low-level addXXs; find_rules interface;

added 'sym' and 'symmetric' atts;

removed bang_args;

'symmetric' attribute moved to Pure/calculation.ML;

simplified (and clarified) integration with Pure/ContextRules; removed "extra" rules as separate slots, only keep xtra_netpair for single-step view of plain haz/safe rules;

iff?: refer to Pure/ContextRules;

ContextRules.intro_bang_global;

added add_rule, del_rule;

tuned declarations;

tuned;

added ex/First_Order_Logic.thy, ex/document/root.tex;

added First_Order_Logic.thy;

sym declarations; tuned declarations;

removed declaration of disjI1, disjI2 (already done in IFOL);

removed AddXIs, AddXEs, AddXDs;

updated;

* Pure/Provers/classical: simplified integration with pure rule attributes and methods;

reactivate tracing markup;

made SML/NJ happy;

made slightly more robust;

added Higher_Order_Logic.thy;

rules_tac: SELECT_GOAL!!; tuned;

disable markup of tracing output (tmp?);

\usepackage{textcomp};

removed \newcommand{\isasymone};