2001-12-10 berghofe 2001-12-10 Replaced several occurrences of "blast" by "rules".
2001-12-10 wenzelm 2001-12-10 document root;
2001-12-09 kleing 2001-12-09 tuned
2001-12-09 kleing 2001-12-09 HOLCF/IMP converted to Isar
2001-12-09 kleing 2001-12-09 HOL/IMP converted to Isar
2001-12-09 kleing 2001-12-09 converted to Isar
2001-12-09 kleing 2001-12-09 latex output setup
2001-12-09 kleing 2001-12-09 tuned for latex output
2001-12-09 kleing 2001-12-09 setup [trans] rules for calculational Isar reasoning
2001-12-08 wenzelm 2001-12-08 use /var/tmp (which happens to be more spacious on atbroy37);
2001-12-08 wenzelm 2001-12-08 new-style theory; proper declarations of various induction rules;
2001-12-08 wenzelm 2001-12-08 added Main.ML;
2001-12-08 wenzelm 2001-12-08 restart_loader: do *not* ThyLoad.reset_path;
2001-12-08 wenzelm 2001-12-08 tuned print_state interfaces;
2001-12-08 wenzelm 2001-12-08 optional PGML markup;
2001-12-08 wenzelm 2001-12-08 added writelns;
2001-12-08 wenzelm 2001-12-08 use "xml.ML";
2001-12-08 wenzelm 2001-12-08 export writeln_default; tuned prefix_lines;
2001-12-08 wenzelm 2001-12-08 tuned print_goals interfaces;
2001-12-08 wenzelm 2001-12-08 added General/xml.ML;
2001-12-08 wenzelm 2001-12-08 Basic support for XML output.
2001-12-07 paulson 2001-12-07 Slightly generalized the agents' knowledge theorems
2001-12-06 wenzelm 2001-12-06 added default_type;
2001-12-06 wenzelm 2001-12-06 tuned line breaks in HTML source;
2001-12-06 wenzelm 2001-12-06 fixed dest atts;
2001-12-06 wenzelm 2001-12-06 refrain from peeking at tags;
2001-12-06 wenzelm 2001-12-06 include session graph;
2001-12-06 paulson 2001-12-06 replaced record_split by the cases method
2001-12-06 paulson 2001-12-06 intro and elim now require arguments
2001-12-06 paulson 2001-12-06 record extend and truncate exercises
2001-12-06 wenzelm 2001-12-06 use Main;
2001-12-06 wenzelm 2001-12-06 * 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;
2001-12-06 wenzelm 2001-12-06 Syntax.internal thesis;
2001-12-06 wenzelm 2001-12-06 tuned xtra_netpair;
2001-12-06 wenzelm 2001-12-06 clarified sym_del;
2001-12-06 wenzelm 2001-12-06 added 'swapped' attribute; tuned xtra_netpair; tuned;
2001-12-06 wenzelm 2001-12-06 added the_mk_cases;
2001-12-06 wenzelm 2001-12-06 tuned;
2001-12-06 wenzelm 2001-12-06 renamed Finite to Finite_Set;
2001-12-06 wenzelm 2001-12-06 less_induct, wf_induct_rule;
2001-12-06 wenzelm 2001-12-06 renamed theory Finite to Finite_Set and converted;
2001-12-06 wenzelm 2001-12-06 this material already part of HOL/Set.thy;
2001-12-05 wenzelm 2001-12-05 sym [sym];
2001-12-05 wenzelm 2001-12-05 tuned;
2001-12-05 wenzelm 2001-12-05 iff;
2001-12-05 wenzelm 2001-12-05 updated;
2001-12-05 wenzelm 2001-12-05 adapted intr/elim uses;
2001-12-05 wenzelm 2001-12-05 eliminated old use of intro/elim method; tuned;
2001-12-05 wenzelm 2001-12-05 simplified proof (no longer use swapped rules);
2001-12-05 wenzelm 2001-12-05 fixed intro steps;
2001-12-05 wenzelm 2001-12-05 tuned declarations (rules, sym, etc.);
2001-12-05 wenzelm 2001-12-05 removed unused functionality (weight etc.);
2001-12-05 wenzelm 2001-12-05 simple version of 'intro' and 'elim' method; use ContextRules.find_rules;
2001-12-05 wenzelm 2001-12-05 added 'print_rules' command;
2001-12-05 wenzelm 2001-12-05 added print_rules;
2001-12-05 wenzelm 2001-12-05 simplified NetRules;
2001-12-05 wenzelm 2001-12-05 export low-level addXXs; find_rules interface;
2001-12-05 wenzelm 2001-12-05 added 'sym' and 'symmetric' atts;
2001-12-05 wenzelm 2001-12-05 removed bang_args;
2001-12-05 wenzelm 2001-12-05 'symmetric' attribute moved to Pure/calculation.ML;