2000-07-30 wenzelm 2000-07-30 updated ObtainFun;
2000-07-30 wenzelm 2000-07-30 'def': no constraint on variable;
2000-07-30 wenzelm 2000-07-30 exporter setup for context elements;
2000-07-30 wenzelm 2000-07-30 export RANGE, hard_asm_tac, soft_asm_tac; export is_chain, assert_forward_or_chain; added the_fact; updated ProofContext.export_wrt;
2000-07-30 wenzelm 2000-07-30 turned into plain context element; exporter setup;
2000-07-30 wenzelm 2000-07-30 local_def(_i): no constraint on var; exporter setup;
2000-07-30 wenzelm 2000-07-30 local_def(_i): no constraint on var;
2000-07-30 wenzelm 2000-07-30 def: no constraint on var;
2000-07-30 wenzelm 2000-07-30 added is_judgment; removed atomic_thesis;
2000-07-30 wenzelm 2000-07-30 ObtainFun (generalized existence reasoning);
2000-07-30 wenzelm 2000-07-30 ThmDeps.enable;
2000-07-30 wenzelm 2000-07-30 added sign_of_cterm;
2000-07-30 wenzelm 2000-07-30 Logic.goal_const;
2000-07-28 wenzelm 2000-07-28 replaced "Sessions" by "Root";
2000-07-28 nipkow 2000-07-28 apply. -> by
2000-07-28 nipkow 2000-07-28 * HOL/While
2000-07-27 wenzelm 2000-07-27 added theory While;
2000-07-27 wenzelm 2000-07-27 export has_internal; tag some rules as internal;
2000-07-27 wenzelm 2000-07-27 added thm_deps;
2000-07-27 wenzelm 2000-07-27 added enter_forward_proof;
2000-07-27 wenzelm 2000-07-27 export write_graph;
2000-07-27 wenzelm 2000-07-27 begin_theory: store *copy* of initial theory;
2000-07-27 wenzelm 2000-07-27 tuned;
2000-07-27 wenzelm 2000-07-27 intro_elim_tac: bimatch_from;
2000-07-26 nipkow 2000-07-26 While functional for defining tail-recursive functions
2000-07-26 nipkow 2000-07-26 *** empty log message ***
2000-07-25 wenzelm 2000-07-25 tuned msg;
2000-07-25 berghofe 2000-07-25 Corrected example which still used old primrec syntax.
2000-07-25 nipkow 2000-07-25 Replaced force by fast because force may now take forever to fail (due to a recend change of David's)
2000-07-25 nipkow 2000-07-25 new constant same_fst
2000-07-25 wenzelm 2000-07-25 by (CLASIMPSET auto_tac);
2000-07-25 wenzelm 2000-07-25 added clarify method; removed unofficial improper methods;
2000-07-25 wenzelm 2000-07-25 added clarsimp method;
2000-07-25 wenzelm 2000-07-25 tuned;
2000-07-25 wenzelm 2000-07-25 removed slow, slow_best methods; added clarify, clarsimp methods;
2000-07-25 wenzelm 2000-07-25 * Isar/Provers: intro/elim/dest attributes: changed intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one should have to change intro!! to intro? only);
2000-07-25 wenzelm 2000-07-25 rearranged setup of arithmetic procedures, avoiding global reference values;
2000-07-25 wenzelm 2000-07-25 lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
2000-07-25 wenzelm 2000-07-25 do nat pass theory value, but sg_ref;
2000-07-25 wenzelm 2000-07-25 avoid referencing thy value; rename_numerals: use implicit theory context; eliminated some simpset_of Int.thy (why needed anyway?);
2000-07-25 wenzelm 2000-07-25 avoid referencing thy value; rename_numerals: use implicit theory context;
2000-07-25 wenzelm 2000-07-25 tuned deps;
2000-07-24 wenzelm 2000-07-24 tuned;
2000-07-24 wenzelm 2000-07-24 changed deps;
2000-07-24 wenzelm 2000-07-24 rename_numerals: use implicit theory context;
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value; lemma_prat_add_mult_mono moved to PRat.ML;
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value; lemma_prat_add_mult_mono moved here;
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value; rename_numerals: use implicit theory context; avoid some simpset_of Int.thy (why needed anyway?);
2000-07-24 wenzelm 2000-07-24 simpset_of NatDef.thy (why anyway?);
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value; rename_numerals: use implicit theory context;
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value;
2000-07-24 wenzelm 2000-07-24 tuned comment;
2000-07-24 wenzelm 2000-07-24 avoid global references;
2000-07-24 wenzelm 2000-07-24 do not pass theory values, but sg_ref;
2000-07-24 wenzelm 2000-07-24 Drule.merge_rules;
2000-07-23 wenzelm 2000-07-23 get_names: topologically sorted;
2000-07-23 wenzelm 2000-07-23 removed all_sessions.graph; improved graph 'directories'; tuned;
2000-07-23 wenzelm 2000-07-23 removed all_sessions;
2000-07-23 wenzelm 2000-07-23 disallow duplicates in session identifiers;
2000-07-23 wenzelm 2000-07-23 assimilated;