Thu, 19 Jun 2008 20:48:00 +0200 wenzelm tuned signature;
Thu, 19 Jun 2008 20:47:58 +0200 wenzelm removed duplicate of DatatypePackage.read_typ;
Thu, 19 Jun 2008 20:34:28 +0200 huffman add lemma cfcomp_LAM
Thu, 19 Jun 2008 17:32:18 +0200 wenzelm add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);
Thu, 19 Jun 2008 15:47:26 +0200 urbanc slightly tuned
Thu, 19 Jun 2008 11:46:14 +0200 krauss generalized induct_scheme method to prove conditional induction schemes.
Thu, 19 Jun 2008 00:02:08 +0200 huffman add lemma iterate_iterate
Wed, 18 Jun 2008 23:15:41 +0200 wenzelm * Disposed old term read functions;
Wed, 18 Jun 2008 23:07:30 +0200 huffman replace preorder class with locale
Wed, 18 Jun 2008 23:03:11 +0200 huffman add lemma compact_imp_principal to locale ideal_completion
Wed, 18 Jun 2008 22:32:06 +0200 wenzelm added type_constraint (formerly in type_infer.ML, which is now loaded later);
Wed, 18 Jun 2008 22:32:04 +0200 wenzelm TypeExt.type_constraint;
Wed, 18 Jun 2008 22:32:03 +0200 wenzelm simplified TypeInfer.infer_types;
Wed, 18 Jun 2008 22:32:02 +0200 wenzelm improved error output -- variant/mark bounds;
Wed, 18 Jun 2008 22:32:01 +0200 wenzelm load type_infer.ML after Syntax module;
Wed, 18 Jun 2008 18:55:10 +0200 wenzelm eliminated old Sign.read_term/Thm.read_cterm etc.;
Wed, 18 Jun 2008 18:55:08 +0200 wenzelm moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
Wed, 18 Jun 2008 18:55:07 +0200 wenzelm export transfer_syntax;
Wed, 18 Jun 2008 18:55:06 +0200 wenzelm moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
Wed, 18 Jun 2008 18:55:05 +0200 wenzelm removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
Wed, 18 Jun 2008 18:55:04 +0200 wenzelm added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
Wed, 18 Jun 2008 18:55:03 +0200 wenzelm removed obsolete read_def_cterms/read_cterm;
Wed, 18 Jun 2008 18:55:02 +0200 wenzelm load proof term operations later;
Wed, 18 Jun 2008 18:55:01 +0200 wenzelm more antiquotations;
Wed, 18 Jun 2008 18:55:00 +0200 wenzelm OldGoals.read_prop;
Wed, 18 Jun 2008 18:54:59 +0200 wenzelm OldGoals.simple_read_term;
Wed, 18 Jun 2008 18:54:57 +0200 wenzelm simplified Abel_Cancel setup;
Wed, 18 Jun 2008 16:55:44 +0200 wenzelm updated generated file;
Wed, 18 Jun 2008 16:55:21 +0200 wenzelm pervasive cut_inst_tac;
Tue, 17 Jun 2008 04:19:50 +0200 urbanc added a progress lemma and tuned some comments
Mon, 16 Jun 2008 22:20:59 +0200 wenzelm * Rules and tactics that read instantiations now demand a proper context;
Mon, 16 Jun 2008 22:13:54 +0200 wenzelm added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML);
Mon, 16 Jun 2008 22:13:52 +0200 wenzelm renamed rename_params_tac to rename_tac;
Mon, 16 Jun 2008 22:13:50 +0200 wenzelm removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
Mon, 16 Jun 2008 22:13:49 +0200 wenzelm removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm;
Mon, 16 Jun 2008 22:13:47 +0200 wenzelm removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);
Mon, 16 Jun 2008 22:13:46 +0200 wenzelm inst1_tac: proper context;
Mon, 16 Jun 2008 22:13:39 +0200 wenzelm pervasive RuleInsts;
Mon, 16 Jun 2008 17:56:08 +0200 wenzelm updated generated file;
Mon, 16 Jun 2008 17:54:51 +0200 wenzelm converted ML proofs;
Mon, 16 Jun 2008 17:54:50 +0200 wenzelm added read_instantiate;
Mon, 16 Jun 2008 17:54:49 +0200 wenzelm ML tactic: do not abstract over context again;
Mon, 16 Jun 2008 17:54:48 +0200 wenzelm export eof;
Mon, 16 Jun 2008 17:54:47 +0200 wenzelm removed obsolete inst;
Mon, 16 Jun 2008 17:54:46 +0200 wenzelm atomize: proper context;
Mon, 16 Jun 2008 17:54:45 +0200 wenzelm atomize: proper context;
Mon, 16 Jun 2008 17:54:43 +0200 wenzelm RuleInsts.read_instantiate;
Mon, 16 Jun 2008 17:54:42 +0200 wenzelm ptac/prolog_tac: proper context;
Mon, 16 Jun 2008 17:54:39 +0200 wenzelm allE_Nil: only one copy, proven in regular theory source;
Mon, 16 Jun 2008 17:54:38 +0200 wenzelm deriv_tac/DERIV_tac: proper context;
Mon, 16 Jun 2008 17:54:36 +0200 wenzelm sum3_instantiate: proper context;
Mon, 16 Jun 2008 17:54:35 +0200 wenzelm eliminated OldGoals.inst;
Mon, 16 Jun 2008 14:18:55 +0200 wenzelm updated generated file;
Mon, 16 Jun 2008 14:18:45 +0200 wenzelm method "tactic": only "facts" as bound value;
Mon, 16 Jun 2008 11:47:46 +0200 chaieb Export a wrapper for all semiring_normalizers
Sat, 14 Jun 2008 23:52:51 +0200 wenzelm proper context for tactics derived from res_inst_tac;
Sat, 14 Jun 2008 23:33:43 +0200 wenzelm added ~: and ~=;
Sat, 14 Jun 2008 23:20:12 +0200 wenzelm export subgoal_tac, subgoals_tac, thin_tac;
Sat, 14 Jun 2008 23:20:11 +0200 wenzelm prove: full Variable.declare_term, including constraints;
Sat, 14 Jun 2008 23:20:10 +0200 wenzelm prove_standard: more precises argument passing;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip