isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

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

Tue, 25 Sep 2007 13:42:59 +0200 size hook

haftmann [Tue, 25 Sep 2007 13:42:59 +0200] rev 24710

size hook

Tue, 25 Sep 2007 13:28:42 +0200 removed redundant global_parse operations;

wenzelm [Tue, 25 Sep 2007 13:28:42 +0200] rev 24709

removed redundant global_parse operations; renamed global_XXX to XXX_global;

Tue, 25 Sep 2007 13:28:41 +0200 Syntax.parse/check/read;

wenzelm [Tue, 25 Sep 2007 13:28:41 +0200] rev 24708

Syntax.parse/check/read; no export of read/cert_axm;

Tue, 25 Sep 2007 13:28:37 +0200 Syntax.parse/check/read;

wenzelm [Tue, 25 Sep 2007 13:28:37 +0200] rev 24707

Syntax.parse/check/read;

Tue, 25 Sep 2007 13:28:35 +0200 * Pure/Syntax: generic interfaces for parsing and type checking;

wenzelm [Tue, 25 Sep 2007 13:28:35 +0200] rev 24706

* Pure/Syntax: generic interfaces for parsing and type checking; tuned;

Tue, 25 Sep 2007 12:59:24 +0200 Simplified proof due to improved integration of order_tac and simp.

ballarin [Tue, 25 Sep 2007 12:59:24 +0200] rev 24705

Simplified proof due to improved integration of order_tac and simp.

Tue, 25 Sep 2007 12:56:27 +0200 Transitivity reasoner gets additional argument of premises to improve integration with simplifier.

ballarin [Tue, 25 Sep 2007 12:56:27 +0200] rev 24704

Transitivity reasoner gets additional argument of premises to improve integration with simplifier.

Tue, 25 Sep 2007 12:16:15 +0200 dropped

haftmann [Tue, 25 Sep 2007 12:16:15 +0200] rev 24703

dropped

Tue, 25 Sep 2007 12:16:14 +0200 ML monad support

haftmann [Tue, 25 Sep 2007 12:16:14 +0200] rev 24702

ML monad support

Tue, 25 Sep 2007 12:16:13 +0200 no cleverness for instance parameters

haftmann [Tue, 25 Sep 2007 12:16:13 +0200] rev 24701

no cleverness for instance parameters

Tue, 25 Sep 2007 12:16:12 +0200 added conversions for natural numbers

haftmann [Tue, 25 Sep 2007 12:16:12 +0200] rev 24700

added conversions for natural numbers

Tue, 25 Sep 2007 12:16:08 +0200 datatype interpretators for size and datatype_realizer

haftmann [Tue, 25 Sep 2007 12:16:08 +0200] rev 24699

datatype interpretators for size and datatype_realizer

Tue, 25 Sep 2007 10:27:43 +0200 hide successor

nipkow [Tue, 25 Sep 2007 10:27:43 +0200] rev 24698

hide successor

Mon, 24 Sep 2007 22:00:18 +0200 fixed haftmann bug

nipkow [Mon, 24 Sep 2007 22:00:18 +0200] rev 24697

fixed haftmann bug

Mon, 24 Sep 2007 21:07:41 +0200 added @{theory_ref};

wenzelm [Mon, 24 Sep 2007 21:07:41 +0200] rev 24696

added @{theory_ref};

Mon, 24 Sep 2007 21:07:40 +0200 added @{type_name};

wenzelm [Mon, 24 Sep 2007 21:07:40 +0200] rev 24695

added @{type_name};

Mon, 24 Sep 2007 21:07:39 +0200 added polymorphic_types;

wenzelm [Mon, 24 Sep 2007 21:07:39 +0200] rev 24694

added polymorphic_types;

Mon, 24 Sep 2007 21:07:38 +0200 eliminated ProofContext.read_termTs;

wenzelm [Mon, 24 Sep 2007 21:07:38 +0200] rev 24693

eliminated ProofContext.read_termTs;

Mon, 24 Sep 2007 21:07:36 +0200 more ML antiqs;

wenzelm [Mon, 24 Sep 2007 21:07:36 +0200] rev 24692

more ML antiqs;

Mon, 24 Sep 2007 19:34:55 +0200 localized { .. } (but only a few thms)

nipkow [Mon, 24 Sep 2007 19:34:55 +0200] rev 24691

localized { .. } (but only a few thms)

Mon, 24 Sep 2007 13:53:26 +0200 renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;

wenzelm [Mon, 24 Sep 2007 13:53:26 +0200] rev 24690

renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;

Mon, 24 Sep 2007 13:52:51 +0200 renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;

wenzelm [Mon, 24 Sep 2007 13:52:51 +0200] rev 24689

renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML; replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);

Mon, 24 Sep 2007 13:52:50 +0200 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);

wenzelm [Mon, 24 Sep 2007 13:52:50 +0200] rev 24688

replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);

Sun, 23 Sep 2007 23:39:42 +0200 removed dead code;

wenzelm [Sun, 23 Sep 2007 23:39:42 +0200] rev 24687

removed dead code; tuned;

Sun, 23 Sep 2007 23:00:01 +0200 made smlnj happy;

wenzelm [Sun, 23 Sep 2007 23:00:01 +0200] rev 24686

made smlnj happy;

Sun, 23 Sep 2007 22:23:37 +0200 tuned @{cpat};

wenzelm [Sun, 23 Sep 2007 22:23:37 +0200] rev 24685

tuned @{cpat};

Sun, 23 Sep 2007 22:23:35 +0200 added read_term_pattern/schematic/abbrev;

wenzelm [Sun, 23 Sep 2007 22:23:35 +0200] rev 24684

added read_term_pattern/schematic/abbrev; prepare_patterns: Variable.polymorphic; removed obsolete cert/pats versions;

Sun, 23 Sep 2007 22:23:34 +0200 ProofContext.read_term_pattern;

wenzelm [Sun, 23 Sep 2007 22:23:34 +0200] rev 24683

ProofContext.read_term_pattern;

Sun, 23 Sep 2007 22:23:33 +0200 constrain: canonical argument order;

wenzelm [Sun, 23 Sep 2007 22:23:33 +0200] rev 24682

constrain: canonical argument order; removed obsolete logicT;

Sun, 23 Sep 2007 22:23:31 +0200 tuned;

wenzelm [Sun, 23 Sep 2007 22:23:31 +0200] rev 24681

tuned;

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

isabelle