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};