Tue, 25 Sep 2007 13:28:41 +0200 wenzelm Syntax.parse/check/read;
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Tue, 25 Sep 2007 13:28:35 +0200 wenzelm * Pure/Syntax: generic interfaces for parsing and type checking;
Tue, 25 Sep 2007 12:59:24 +0200 ballarin Simplified proof due to improved integration of order_tac and simp.
Tue, 25 Sep 2007 12:56:27 +0200 ballarin Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
Tue, 25 Sep 2007 12:16:15 +0200 haftmann dropped
Tue, 25 Sep 2007 12:16:14 +0200 haftmann ML monad support
Tue, 25 Sep 2007 12:16:13 +0200 haftmann no cleverness for instance parameters
Tue, 25 Sep 2007 12:16:12 +0200 haftmann added conversions for natural numbers
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Tue, 25 Sep 2007 10:27:43 +0200 nipkow hide successor
Mon, 24 Sep 2007 22:00:18 +0200 nipkow fixed haftmann bug
Mon, 24 Sep 2007 21:07:41 +0200 wenzelm added @{theory_ref};
Mon, 24 Sep 2007 21:07:40 +0200 wenzelm added @{type_name};
Mon, 24 Sep 2007 21:07:39 +0200 wenzelm added polymorphic_types;
Mon, 24 Sep 2007 21:07:38 +0200 wenzelm eliminated ProofContext.read_termTs;
Mon, 24 Sep 2007 21:07:36 +0200 wenzelm more ML antiqs;
Mon, 24 Sep 2007 19:34:55 +0200 nipkow localized { .. } (but only a few thms)
Mon, 24 Sep 2007 13:53:26 +0200 wenzelm renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
Mon, 24 Sep 2007 13:52:51 +0200 wenzelm renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
Mon, 24 Sep 2007 13:52:50 +0200 wenzelm replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
Sun, 23 Sep 2007 23:39:42 +0200 wenzelm removed dead code;
Sun, 23 Sep 2007 23:00:01 +0200 wenzelm made smlnj happy;
Sun, 23 Sep 2007 22:23:37 +0200 wenzelm tuned @{cpat};
Sun, 23 Sep 2007 22:23:35 +0200 wenzelm added read_term_pattern/schematic/abbrev;
Sun, 23 Sep 2007 22:23:34 +0200 wenzelm ProofContext.read_term_pattern;
Sun, 23 Sep 2007 22:23:33 +0200 wenzelm constrain: canonical argument order;
Sun, 23 Sep 2007 22:23:31 +0200 wenzelm tuned;
Sun, 23 Sep 2007 22:23:27 +0200 wenzelm TypeInfer.constrain: canonical argument order;
Sun, 23 Sep 2007 22:23:24 +0200 wenzelm tuned ML setup;
Sun, 23 Sep 2007 22:11:50 +0200 urbanc tuned one proof so to not run in a loop with the new atom-representation
Sun, 23 Sep 2007 22:10:27 +0200 urbanc changed the representation of atoms to datatypes over nats
Sat, 22 Sep 2007 17:45:58 +0200 wenzelm ProofContext.mode_abbrev;
Sat, 22 Sep 2007 17:45:57 +0200 wenzelm removed obsolete set_expand_abbrevs (superceded by mode_abbrev);
Sat, 22 Sep 2007 17:45:56 +0200 wenzelm certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;
Sat, 22 Sep 2007 17:45:55 +0200 wenzelm certify: do_expand as explicit argument, actually certify type of abstractions;
Fri, 21 Sep 2007 22:51:13 +0200 wenzelm tuned;
Fri, 21 Sep 2007 22:51:12 +0200 wenzelm added has_abs (from envir.ML);
Fri, 21 Sep 2007 22:51:10 +0200 wenzelm Term.has_abs;
Fri, 21 Sep 2007 22:51:08 +0200 wenzelm proper signature constraint;
Thu, 20 Sep 2007 20:58:40 +0200 wenzelm added interrupt_timeout;
Thu, 20 Sep 2007 20:56:54 +0200 wenzelm Generic interpretation of theory data.
Thu, 20 Sep 2007 20:56:34 +0200 wenzelm tuned signature;
Thu, 20 Sep 2007 20:56:33 +0200 wenzelm avoid Theory.rep_theory;
Thu, 20 Sep 2007 20:56:32 +0200 wenzelm added interpretation.ML;
Thu, 20 Sep 2007 17:48:16 +0200 wenzelm improved error behaviour of use (bootstrap version);
Thu, 20 Sep 2007 16:37:34 +0200 haftmann more precise treatment of free dictionary parameters for evaluation
Thu, 20 Sep 2007 16:37:33 +0200 haftmann fixed cg setup
Thu, 20 Sep 2007 16:37:32 +0200 haftmann restored ml system independence
Thu, 20 Sep 2007 16:37:31 +0200 haftmann more permissive
Thu, 20 Sep 2007 16:37:30 +0200 haftmann clarified code lemmas
Thu, 20 Sep 2007 16:37:29 +0200 haftmann fixed wrong syntax treatment in class target
Thu, 20 Sep 2007 16:37:28 +0200 haftmann code lemmas for cardinality
Thu, 20 Sep 2007 16:23:12 +0200 berghofe - eval_term no longer computes result during compile time
Thu, 20 Sep 2007 12:10:23 +0200 obua improved computing
Thu, 20 Sep 2007 12:09:09 +0200 obua changed lemmas
Wed, 19 Sep 2007 20:45:29 +0200 wenzelm ml_output: proper error instead of error_msg;
Wed, 19 Sep 2007 18:48:54 +0200 webertj comment added to explain a potential scheduling problem
Wed, 19 Sep 2007 17:16:40 +0200 nipkow tuned
Wed, 19 Sep 2007 15:26:58 +0200 nipkow *** empty log message ***
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip