isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

Tue, 08 Aug 2006 08:19:06 +0200 added Tools/typedef_codegen.ML

haftmann [Tue, 08 Aug 2006 08:19:06 +0200] rev 20349

added Tools/typedef_codegen.ML

Tue, 08 Aug 2006 08:18:59 +0200 abandoned equal_list in favor for eq_list

haftmann [Tue, 08 Aug 2006 08:18:59 +0200] rev 20348

abandoned equal_list in favor for eq_list

Mon, 07 Aug 2006 17:43:51 +0200 Simple ML script for producing Gnuplot files from

berghofe [Mon, 07 Aug 2006 17:43:51 +0200] rev 20347

Simple ML script for producing Gnuplot files from isatest log files.

Mon, 07 Aug 2006 03:10:38 +0200 title fixed

webertj [Mon, 07 Aug 2006 03:10:38 +0200] rev 20346

title fixed

Sat, 05 Aug 2006 15:15:07 +0200 updated;

wenzelm [Sat, 05 Aug 2006 15:15:07 +0200] rev 20345

updated;

Sat, 05 Aug 2006 14:55:09 +0200 avoid low-level tsig;

wenzelm [Sat, 05 Aug 2006 14:55:09 +0200] rev 20344

avoid low-level tsig;

Sat, 05 Aug 2006 14:52:58 +0200 reworked read_instantiate -- separate read_insts;

wenzelm [Sat, 05 Aug 2006 14:52:58 +0200] rev 20343

reworked read_instantiate -- separate read_insts;

Sat, 05 Aug 2006 14:52:57 +0200 tuned;

wenzelm [Sat, 05 Aug 2006 14:52:57 +0200] rev 20342

tuned;

Sat, 05 Aug 2006 14:52:55 +0200 removed obsolete sign_of;

wenzelm [Sat, 05 Aug 2006 14:52:55 +0200] rev 20341

removed obsolete sign_of;

Sat, 05 Aug 2006 14:52:53 +0200 Amine Chaieb: experimental generic reflection and reification in HOL;

wenzelm [Sat, 05 Aug 2006 14:52:53 +0200] rev 20340

Amine Chaieb: experimental generic reflection and reification in HOL;

Sat, 05 Aug 2006 00:52:17 +0200 use atbroy101 instead of atbroy98 (freezes up)

isatest [Sat, 05 Aug 2006 00:52:17 +0200] rev 20339

use atbroy101 instead of atbroy98 (freezes up)

Fri, 04 Aug 2006 18:01:45 +0200 Added Keywords: "otherwise" and "sequential", needed for function package's

krauss [Fri, 04 Aug 2006 18:01:45 +0200] rev 20338

Added Keywords: "otherwise" and "sequential", needed for function package's sequential mode.

Fri, 04 Aug 2006 12:01:31 +0200 *** empty log message ***

chaieb [Fri, 04 Aug 2006 12:01:31 +0200] rev 20337

*** empty log message ***

Thu, 03 Aug 2006 17:30:44 +0200 Rule instantiations -- operations within a rule/subgoal context.

wenzelm [Thu, 03 Aug 2006 17:30:44 +0200] rev 20336

Rule instantiations -- operations within a rule/subgoal context.

Thu, 03 Aug 2006 17:30:43 +0200 moved bires_inst_tac etc. to rule_insts.ML;

wenzelm [Thu, 03 Aug 2006 17:30:43 +0200] rev 20335

moved bires_inst_tac etc. to rule_insts.ML;

Thu, 03 Aug 2006 17:30:42 +0200 moved read_instantiate etc. to rule_insts.ML;

wenzelm [Thu, 03 Aug 2006 17:30:42 +0200] rev 20334

moved read_instantiate etc. to rule_insts.ML;

Thu, 03 Aug 2006 17:30:41 +0200 added Isar/rule_insts.ML;

wenzelm [Thu, 03 Aug 2006 17:30:41 +0200] rev 20333

added Isar/rule_insts.ML;

Thu, 03 Aug 2006 17:30:40 +0200 removed obsolete commute, map_list;

wenzelm [Thu, 03 Aug 2006 17:30:40 +0200] rev 20332

removed obsolete commute, map_list;

Thu, 03 Aug 2006 17:30:39 +0200 removed obsolete add_term_tvarnames;

wenzelm [Thu, 03 Aug 2006 17:30:39 +0200] rev 20331

removed obsolete add_term_tvarnames;

Thu, 03 Aug 2006 17:30:38 +0200 tuned;

wenzelm [Thu, 03 Aug 2006 17:30:38 +0200] rev 20330

tuned;

Thu, 03 Aug 2006 17:30:37 +0200 tuned types_sorts, add_used;

wenzelm [Thu, 03 Aug 2006 17:30:37 +0200] rev 20329

tuned types_sorts, add_used;

Thu, 03 Aug 2006 17:30:36 +0200 RuleInsts.bires_inst_tac;

wenzelm [Thu, 03 Aug 2006 17:30:36 +0200] rev 20328

RuleInsts.bires_inst_tac;

Thu, 03 Aug 2006 15:58:04 +0200 *** empty log message ***

chaieb [Thu, 03 Aug 2006 15:58:04 +0200] rev 20327

*** empty log message ***

Thu, 03 Aug 2006 15:14:05 +0200 fixed generator

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;

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);

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);

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);

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;

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);

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).

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.

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.

ballarin [Thu, 03 Aug 2006 14:53:57 +0200] rev 20317

Updated comments.

Thu, 03 Aug 2006 14:53:35 +0200 updated;

wenzelm [Thu, 03 Aug 2006 14:53:35 +0200] rev 20316

updated;

Wed, 02 Aug 2006 23:09:49 +0200 tuned proofs;

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);

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;

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;

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);

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;

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;

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;

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.;

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;

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;

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.;

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;

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;

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;

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;

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;

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.;

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;

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;

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;

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;

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;

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;

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;

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;

wenzelm [Wed, 02 Aug 2006 22:26:44 +0200] rev 20290

normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export; tuned;

(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle