Thu, 27 Sep 2007 17:22:15 +0200 wenzelm some more simultaneous use_thys;
Thu, 27 Sep 2007 11:46:05 +0200 wenzelm read: explicit treatment of scanner failure;
Wed, 26 Sep 2007 22:38:11 +0200 wenzelm tuned;
Wed, 26 Sep 2007 22:28:00 +0200 wenzelm tuned;
Wed, 26 Sep 2007 22:27:44 +0200 wenzelm tuned;
Wed, 26 Sep 2007 22:21:05 +0200 wenzelm * Pure/Isar: unified specification syntax admits type inference and dummy patterns;
Wed, 26 Sep 2007 22:21:02 +0200 wenzelm read/check_specification: free_dummy_patterns;
Wed, 26 Sep 2007 22:20:59 +0200 wenzelm added free_dummy_patterns;
Wed, 26 Sep 2007 20:50:34 +0200 wenzelm added minimize_sort, complete_sort;
Wed, 26 Sep 2007 20:50:33 +0200 wenzelm Sign.minimize/complete_sort;
Wed, 26 Sep 2007 20:27:58 +0200 haftmann convenient obtain rule for sets
Wed, 26 Sep 2007 20:27:57 +0200 haftmann added code lemma for 1
Wed, 26 Sep 2007 20:27:55 +0200 haftmann moved Finite_Set before Datatype
Wed, 26 Sep 2007 19:19:38 +0200 wenzelm adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);
Wed, 26 Sep 2007 19:18:01 +0200 wenzelm Attrib.eval_thms;
Wed, 26 Sep 2007 19:18:00 +0200 wenzelm Attrib.eval_thms;
Wed, 26 Sep 2007 19:17:59 +0200 wenzelm read/check_specification: proper type inference across multiple sections, result is in closed form;
Wed, 26 Sep 2007 19:17:58 +0200 wenzelm added eval_thms;
Wed, 26 Sep 2007 19:17:57 +0200 wenzelm minimal adaptions for Specification.read/check_specification;
Wed, 26 Sep 2007 19:17:56 +0200 wenzelm proper Specification.read_specification;
Wed, 26 Sep 2007 19:17:55 +0200 wenzelm removed dead code;
Wed, 26 Sep 2007 11:27:46 +0200 wenzelm declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
Wed, 26 Sep 2007 09:05:58 +0200 haftmann made SML/NJ happy
Tue, 25 Sep 2007 21:08:36 +0200 haftmann rudimentary support for Haskell
Tue, 25 Sep 2007 21:08:35 +0200 haftmann added support for Haskell, OCaml
Tue, 25 Sep 2007 21:08:34 +0200 haftmann Efficient_Nat and Pretty_Int integrated with ML_Int
Tue, 25 Sep 2007 17:06:19 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 25 Sep 2007 17:06:18 +0200 wenzelm tuned functor application;
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 25 Sep 2007 15:34:35 +0200 wenzelm simplified interpretation setup;
Tue, 25 Sep 2007 13:42:59 +0200 haftmann size hook
Tue, 25 Sep 2007 13:28:42 +0200 wenzelm removed redundant global_parse operations;
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;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip