Moved sum_case to theory HOL/Datatype.

tuned;

Corrected two busg in the simplifier.

\indexisarreg;

\VVar;

checkpoint;

tuned; fixed HOL-Real;

real numerals;

added HOL-Real; made relocatable;

echo ML_PLATFORM;

activate example;

delcongs [if_weak_cong];

print_context;

eliminated HOL-AxClasses target;

intro (no +);

mucke -res;

if_svc_enabled;

AxClasses, Isar_examples;

intro/elim: REPEAT1;

new theories RealBin, RealInt, RealPow

* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;

quite a lot of tuning and cleanup;

sysman: Stefan Berghofer;

more;

Mucke, Einhoven;

quite a lot of tuning an cleanup;

sum_case_Inl and sum_case_Inr are now defined in Datatype.ML.

Moved sum_case stuff from Sum to Datatype.

real literals using binary arithmetic

new entriues.

updated

disabled print_mode (tmp);

lookup_theory;

defer_recdef

removed needless comments

removed all unnecessary code

now with abstraction code previously in HOL/Tools/svc_funcs.ML

documented svc_tac

finished theories;

renamed 'some_rule' to 'rule';

tuned;

removed fixnumerals (for the time being);

tuned Goal syntax;

improved messages;

really removed -m option;

removed -m option;

usedir: removed -m option;

Method.modifier; fixed 'only:';

Method.modifier;

assume: multiple args;

warn_vars; tuned strings_of_context; assume(_i): multiple args;

assume/presume: and_list1;

sectioned_args etc.: more general modifier;

deps: include 'really' flag;

isa_action: don't lock pretend_used files;

proper writeln of begin_state;

(*no fix_shyps*);

tuned messages;

from Konrad: support for schematic definitions

sum_case renamed to basic_sum_case;

Removed rbeta.

tuned messages;

tuned;

Renamed sum_case to basic_sum_case.

Eliminated some infixes.

Eliminated some infixes.

Renamed sum_case to basic_sum_case and removed translations for sum_case to avoid conflicts with the constant sum_case introduced in Datatype.thy.

tuned;

replaced 'ProofGeneral' by 'Proof General';

Modified section about generation of theory browsing information. Documented new -P option.

new version from Konrad with "lazy" (deferred) definitons

tidied some proofs

new primitive rule permute_prems to underlie defer_tac and rotate_prems

freeze_thaw does nothing if no variables

Added take_all and drop_all to simpset.

eliminated HOL_quantifiers (replaced by "HOL" print mode);

may_load_file; use_thy etc.: warn_finished; added begin_update_theory; added quiet_update_thy;

ThyInfo.may_load_file;

begin_update_theory;

PASS(_MODE): works better without space (why?);

removed HOL_quantifiers;

HOL_quantifiers;

replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);

turned SVC_Oracle into a new-style theory in order to get automatic handling of its additional dependency on Tools/svc_funcs.ML;

Better handling of path for remote theory browsing information.

Goals.reset_goals;

reset_goals;

intro+;

remove tmp files;

tuned;

renamed 'single' to 'some_rule'; added 'intro', 'elim';

renamed Cons to Consq in order to avoid clash with List.Cons;

Tuned some comments.

Path for remote theory browsing information is now stored in referece variable rpath.

-m option;

replaced "op #" by "Cons";