2008-03-29 wenzelm 2008-03-29 simplified PureThy.store_thm;
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-03-29 wenzelm 2008-03-29 * Eliminated destructive theorem database. * Commands 'use' and 'ML' are now purely functional; added diagnostic 'ML_val'.
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (not really needed);
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (turned into proper argument);
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (unused);
2008-03-29 wenzelm 2008-03-29 eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
2008-03-28 wenzelm 2008-03-28 added forget_structure;
2008-03-28 wenzelm 2008-03-28 eval_wrapper: non-critical version via unique Isabelle structure, proper forget_structure;
2008-03-28 wenzelm 2008-03-28 ml_tactic: non-critical version via proof data and thread data;
2008-03-28 wenzelm 2008-03-28 NAMED_CRITICAL;
2008-03-28 haftmann 2008-03-28 unfold_locales now part of default tactic
2008-03-28 haftmann 2008-03-28 import Main explicitly
2008-03-28 haftmann 2008-03-28 dropped now superfluous ad-hoc adaption
2008-03-28 haftmann 2008-03-28 not depends on Main any longer
2008-03-28 haftmann 2008-03-28 accomodated to sledgehammer theory dependency requirement
2008-03-28 haftmann 2008-03-28 only invoke interpret
2008-03-28 wenzelm 2008-03-28 updated generated file;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-28 wenzelm 2008-03-28 avoid rebinding of existing facts;
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 urbanc 2008-03-28 tuned proofs
2008-03-28 wenzelm 2008-03-28 tuned;
2008-03-28 wenzelm 2008-03-28 updated dependencies;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 huffman 2008-03-27 remove commented text
2008-03-27 wenzelm 2008-03-27 avoid ambiguity of State.state vs. JVMType.state;
2008-03-27 huffman 2008-03-27 declare cont_lemmas_ext as simp rules individually
2008-03-27 wenzelm 2008-03-27 avoid amiguity of Continuity.chain vs. Porder.chain;
2008-03-27 wenzelm 2008-03-27 avoid amiguity of State.state vs. JVMType.state;
2008-03-27 haftmann 2008-03-27 changed wrong assignement in signature sections
2008-03-27 haftmann 2008-03-27 clarified character serializations
2008-03-27 haftmann 2008-03-27 added Enum
2008-03-27 haftmann 2008-03-27 circumventing merge problem
2008-03-27 haftmann 2008-03-27 explicit case names for rule list_induct2
2008-03-27 haftmann 2008-03-27 instance for functions, explicit characters
2008-03-27 haftmann 2008-03-27 lemmas about map_of (zip _ _)
2008-03-27 haftmann 2008-03-27 restructuring; explicit case names for rule list_induct2
2008-03-27 haftmann 2008-03-27 no "attach UNIV" any more
2008-03-27 wenzelm 2008-03-27 tuned comments; tuned;
2008-03-27 wenzelm 2008-03-27 tuned comments;
2008-03-27 wenzelm 2008-03-27 fixed theory imports;
2008-03-27 wenzelm 2008-03-27 tuned appendix;
2008-03-27 wenzelm 2008-03-27 removed obsolete appl_syntax, applC_syntax;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-27 wenzelm 2008-03-27 Command 'setup': discontinued implicit version.
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure; renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context; moved old the_context to old_goals.ML;
2008-03-27 wenzelm 2008-03-27 added process_file;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure; implicit setup of emerging theory Pure;
2008-03-27 wenzelm 2008-03-27 moved old the_context here; eliminated theory ProtoPure; renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure; implicit setup of emerging theory Pure; added >>> operator;
2008-03-27 wenzelm 2008-03-27 implicit setup of emerging theory Pure;
2008-03-27 wenzelm 2008-03-27 reduced to theory body (cf. OuterSyntax.process_file);
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2008-03-27 wenzelm 2008-03-27 removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2008-03-27 wenzelm 2008-03-27 HOL (and FOL): renamed variables in rules imp_elim and swap; Eliminated theory ProtoPure.