Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thu, 03 Aug 2006 15:14:05 +0200 fixed generator
changeset
obua [Thu, 03 Aug 2006 15:14:05 +0200] rev 20326
fixed generator
Thu, 03 Aug 2006 15:03:49 +0200 added HOL/ex/Reflection;
changeset
wenzelm [Thu, 03 Aug 2006 15:03:49 +0200] rev 20325
added HOL/ex/Reflection;
Thu, 03 Aug 2006 15:03:11 +0200 removed True_implies (cf. True_implies_equals);
changeset
wenzelm [Thu, 03 Aug 2006 15:03:11 +0200] rev 20324
removed True_implies (cf. True_implies_equals); added header;
Thu, 03 Aug 2006 15:03:10 +0200 removed OldGoals.legacy flag (always warn);
changeset
wenzelm [Thu, 03 Aug 2006 15:03:10 +0200] rev 20323
removed OldGoals.legacy flag (always warn); added warning for legacy ML scripts;
Thu, 03 Aug 2006 15:03:09 +0200 removed OldGoals.legacy flag (always warn);
changeset
wenzelm [Thu, 03 Aug 2006 15:03:09 +0200] rev 20322
removed OldGoals.legacy flag (always warn);
Thu, 03 Aug 2006 15:03:08 +0200 tuned;
changeset
wenzelm [Thu, 03 Aug 2006 15:03:08 +0200] rev 20321
tuned;
Thu, 03 Aug 2006 15:03:07 +0200 removed True_implies (cf. True_implies_equals);
changeset
wenzelm [Thu, 03 Aug 2006 15:03:07 +0200] rev 20320
removed True_implies (cf. True_implies_equals);
Thu, 03 Aug 2006 15:03:05 +0200 Generic reflection and reification (by Amine Chaieb).
changeset
wenzelm [Thu, 03 Aug 2006 15:03:05 +0200] rev 20319
Generic reflection and reification (by Amine Chaieb).
Thu, 03 Aug 2006 14:57:26 +0200 Restructured algebra library, added ideals and quotient rings.
changeset
ballarin [Thu, 03 Aug 2006 14:57:26 +0200] rev 20318
Restructured algebra library, added ideals and quotient rings.
Thu, 03 Aug 2006 14:53:57 +0200 Updated comments.
changeset
ballarin [Thu, 03 Aug 2006 14:53:57 +0200] rev 20317
Updated comments.
Thu, 03 Aug 2006 14:53:35 +0200 updated;
changeset
wenzelm [Thu, 03 Aug 2006 14:53:35 +0200] rev 20316
updated;
Wed, 02 Aug 2006 23:09:49 +0200 tuned proofs;
changeset
wenzelm [Wed, 02 Aug 2006 23:09:49 +0200] rev 20315
tuned proofs;
Wed, 02 Aug 2006 22:27:08 +0200 lemma da_good_approx: adapted induction (was exploting lifted obtain result);
changeset
wenzelm [Wed, 02 Aug 2006 22:27:08 +0200] rev 20314
lemma da_good_approx: adapted induction (was exploting lifted obtain result);
Wed, 02 Aug 2006 22:27:07 +0200 renamed Syntax.indexname to Syntax.read_indexname;
changeset
wenzelm [Wed, 02 Aug 2006 22:27:07 +0200] rev 20313
renamed Syntax.indexname to Syntax.read_indexname; added read_int (not Int.fromString, which admits ~ syntax of ML);
Wed, 02 Aug 2006 22:27:06 +0200 tuned;
changeset
wenzelm [Wed, 02 Aug 2006 22:27:06 +0200] rev 20312
tuned;
Wed, 02 Aug 2006 22:27:05 +0200 moved debug option to proof_display.ML (again);
changeset
wenzelm [Wed, 02 Aug 2006 22:27:05 +0200] rev 20311
moved debug option to proof_display.ML (again); normalized Proof.context/method type aliases;
Wed, 02 Aug 2006 22:27:04 +0200 normalized Proof.context/method type aliases;
changeset
wenzelm [Wed, 02 Aug 2006 22:27:04 +0200] rev 20310
normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; prems_limit: < 0 means no output; added debug option (back from proof_display.ML);
Wed, 02 Aug 2006 22:27:03 +0200 simplified Assumption/ProofContext.export;
changeset
wenzelm [Wed, 02 Aug 2006 22:27:03 +0200] rev 20309
simplified Assumption/ProofContext.export; simplified end_block;
Wed, 02 Aug 2006 22:27:02 +0200 added tactical result;
changeset
wenzelm [Wed, 02 Aug 2006 22:27:02 +0200] rev 20308
added tactical result; simplified obtain_export: no Seq.seq, no lifting of result prems; tuned;
Wed, 02 Aug 2006 22:27:01 +0200 removed obsolete Drule.frees/vars_of etc.;
changeset
wenzelm [Wed, 02 Aug 2006 22:27:01 +0200] rev 20307
removed obsolete Drule.frees/vars_of etc.; simplified Assumption/ProofContext.export;
Wed, 02 Aug 2006 22:27:00 +0200 normalized Proof.context/method type aliases;
changeset
wenzelm [Wed, 02 Aug 2006 22:27:00 +0200] rev 20306
normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export;
Wed, 02 Aug 2006 22:26:59 +0200 simplified Proof.end_block;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:59 +0200] rev 20305
simplified Proof.end_block;
Wed, 02 Aug 2006 22:26:58 +0200 removed obsolete Drule.frees/vars_of etc.;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:58 +0200] rev 20304
removed obsolete Drule.frees/vars_of etc.; tuned;
Wed, 02 Aug 2006 22:26:57 +0200 normalized Proof.context/method type aliases;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:57 +0200] rev 20303
normalized Proof.context/method type aliases; added declare/export/import_prf; added focus_subgoal: reset/declare goal schematics;
Wed, 02 Aug 2006 22:26:56 +0200 renamed Syntax.indexname to Syntax.read_indexname;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:56 +0200] rev 20302
renamed Syntax.indexname to Syntax.read_indexname;
Wed, 02 Aug 2006 22:26:55 +0200 Variable.focus_subgoal;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:55 +0200] rev 20301
Variable.focus_subgoal;
Wed, 02 Aug 2006 22:26:54 +0200 replaced maxidx_of_proof by maxidx_proof;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:54 +0200] rev 20300
replaced maxidx_of_proof by maxidx_proof;
Wed, 02 Aug 2006 22:26:53 +0200 prems-limit: int_option;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:53 +0200] rev 20299
prems-limit: int_option;
Wed, 02 Aug 2006 22:26:52 +0200 removed obsolete frees/vars_of etc.;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:52 +0200] rev 20298
removed obsolete frees/vars_of etc.; removed obsolete freeze_all etc.; added norm_hhf_cterm; tuned fold_terms; renamed Syntax.indexname to Syntax.read_indexname;
Wed, 02 Aug 2006 22:26:51 +0200 fake predeclaration of type Proof.context;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:51 +0200] rev 20297
fake predeclaration of type Proof.context;
Wed, 02 Aug 2006 22:26:50 +0200 simplified export: no Seq.seq;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:50 +0200] rev 20296
simplified export: no Seq.seq; normalized Proof.context/method type aliases;
Wed, 02 Aug 2006 22:26:49 +0200 use proper RecdefPackage.get_hints;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:49 +0200] rev 20295
use proper RecdefPackage.get_hints; tuned;
Wed, 02 Aug 2006 22:26:48 +0200 removed obsolete Drule.frees/vars_of;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:48 +0200] rev 20294
removed obsolete Drule.frees/vars_of; renamed thm_vars to thm_varnames;
Wed, 02 Aug 2006 22:26:47 +0200 renamed thm_vars to thm_varnames;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:47 +0200] rev 20293
renamed thm_vars to thm_varnames;
Wed, 02 Aug 2006 22:26:46 +0200 removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:46 +0200] rev 20292
removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;
Wed, 02 Aug 2006 22:26:45 +0200 export get_hints;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:45 +0200] rev 20291
export get_hints; tuned;
Wed, 02 Aug 2006 22:26:44 +0200 normalized Proof.context/method type aliases;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:44 +0200] rev 20290
normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; tuned;
Wed, 02 Aug 2006 22:26:41 +0200 normalized Proof.context/method type aliases;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:41 +0200] rev 20289
normalized Proof.context/method type aliases;
Wed, 02 Aug 2006 22:26:40 +0200 simplified Assumption/ProofContext.export;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:40 +0200] rev 20288
simplified Assumption/ProofContext.export;
Wed, 02 Aug 2006 22:26:39 +0200 replaced obsolete standard/freeze_all by Variable.trade;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:39 +0200] rev 20287
replaced obsolete standard/freeze_all by Variable.trade;
Wed, 02 Aug 2006 22:26:37 +0200 removed obsolete Drule.frees/vars_of etc.;
changeset
wenzelm [Wed, 02 Aug 2006 22:26:37 +0200] rev 20286
removed obsolete Drule.frees/vars_of etc.;
Wed, 02 Aug 2006 18:33:46 +0200 Added type constraint to please sml/nj
changeset
krauss [Wed, 02 Aug 2006 18:33:46 +0200] rev 20285
Added type constraint to please sml/nj
Wed, 02 Aug 2006 18:30:57 +0200 deleted obsolete file
changeset
paulson [Wed, 02 Aug 2006 18:30:57 +0200] rev 20284
deleted obsolete file
Wed, 02 Aug 2006 18:19:48 +0200 lin_arith_prover splits certain operators (e.g. min, max, abs)
changeset
webertj [Wed, 02 Aug 2006 18:19:48 +0200] rev 20283
lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 02 Aug 2006 16:50:41 +0200 lin_arith_prover splits certain operators (e.g. min, max, abs)
changeset
webertj [Wed, 02 Aug 2006 16:50:41 +0200] rev 20282
lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 02 Aug 2006 13:48:21 +0200 Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
changeset
mengj [Wed, 02 Aug 2006 13:48:21 +0200] rev 20281
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.
Wed, 02 Aug 2006 03:33:28 +0200 type annotations fixed (IntInf.int, to make SML/NJ happy)
changeset
webertj [Wed, 02 Aug 2006 03:33:28 +0200] rev 20280
type annotations fixed (IntInf.int, to make SML/NJ happy)
Wed, 02 Aug 2006 01:48:09 +0200 lin_arith_prover splits certain operators (e.g. min, max, abs)
changeset
webertj [Wed, 02 Aug 2006 01:48:09 +0200] rev 20279
lin_arith_prover splits certain operators (e.g. min, max, abs)
Wed, 02 Aug 2006 00:57:41 +0200 proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
changeset
webertj [Wed, 02 Aug 2006 00:57:41 +0200] rev 20278
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
Tue, 01 Aug 2006 15:28:55 +0200 comment (timing information for last example) added
changeset
webertj [Tue, 01 Aug 2006 15:28:55 +0200] rev 20277
comment (timing information for last example) added
Tue, 01 Aug 2006 14:58:43 +0200 possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
changeset
webertj [Tue, 01 Aug 2006 14:58:43 +0200] rev 20276
possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
Tue, 01 Aug 2006 13:51:16 +0200 removed skip
changeset
obua [Tue, 01 Aug 2006 13:51:16 +0200] rev 20275
removed skip
Tue, 01 Aug 2006 13:44:05 +0200 Added in code to check too general axiom clauses.
changeset
mengj [Tue, 01 Aug 2006 13:44:05 +0200] rev 20274
Added in code to check too general axiom clauses.
Tue, 01 Aug 2006 11:32:43 +0200 exported attrib;
changeset
wenzelm [Tue, 01 Aug 2006 11:32:43 +0200] rev 20273
exported attrib;
Mon, 31 Jul 2006 21:06:40 +0200 lin_arith_prover splits certain operators (e.g. min, max, abs)
changeset
webertj [Mon, 31 Jul 2006 21:06:40 +0200] rev 20272
lin_arith_prover splits certain operators (e.g. min, max, abs)
Mon, 31 Jul 2006 20:56:49 +0200 fixed a bug in function poly: decomposition of products
changeset
webertj [Mon, 31 Jul 2006 20:56:49 +0200] rev 20271
fixed a bug in function poly: decomposition of products
(0) -10000 -3000 -1000 -300 -100 -56 +56 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle