Thu, 24 Mar 2011 15:29:31 +0100 bulwahn allowing special set comprehensions in values command; adding an example for special set comprehension in values
Thu, 24 Mar 2011 10:39:47 +0100 bulwahn merged
Wed, 23 Mar 2011 08:50:42 +0100 bulwahn adding documentation about the eval option in quickcheck
Wed, 23 Mar 2011 08:50:40 +0100 bulwahn adapting Quickcheck_Prolog to latest changes
Wed, 23 Mar 2011 08:50:39 +0100 bulwahn changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
Wed, 23 Mar 2011 08:50:32 +0100 bulwahn adapting mutabelle; exporting more Quickcheck functions
Wed, 23 Mar 2011 08:50:31 +0100 bulwahn making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
Wed, 23 Mar 2011 08:50:29 +0100 bulwahn changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
Sat, 26 Mar 2011 12:01:40 +0100 wenzelm added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
Sat, 26 Mar 2011 10:52:29 +0100 wenzelm tuned;
Sat, 26 Mar 2011 10:25:17 +0100 wenzelm dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Thu, 24 Mar 2011 16:47:24 +0100 wenzelm more direct loose_bvar1;
Thu, 24 Mar 2011 13:54:39 +0100 wenzelm indentation;
Thu, 24 Mar 2011 11:45:39 +0100 wenzelm update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
Wed, 23 Mar 2011 21:07:05 +0100 wenzelm added editor mode line;
Wed, 23 Mar 2011 20:57:37 +0100 wenzelm isolate change of Proofterm.proofs in TPTP.thy from rest of session;
Wed, 23 Mar 2011 20:51:36 +0100 wenzelm list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin;
Wed, 23 Mar 2011 16:42:09 +0100 boehmes updated contributed components
Wed, 23 Mar 2011 15:33:17 +0100 boehmes Z3 non-commercial usage may explicitly be declined
Wed, 23 Mar 2011 14:29:29 +0100 boehmes export status function to query whether Z3 has been activated for usage within Isabelle
Wed, 23 Mar 2011 10:38:50 +0100 blanchet merge
Wed, 23 Mar 2011 10:18:42 +0100 blanchet avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
Wed, 23 Mar 2011 10:06:27 +0100 blanchet move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
Wed, 23 Mar 2011 10:21:29 +0100 boehmes really be quiet
Wed, 23 Mar 2011 09:15:49 +0100 krauss replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH
Tue, 22 Mar 2011 21:22:50 +0100 wenzelm merged
Tue, 22 Mar 2011 20:06:10 +0100 hoelzl standardized headers
Tue, 22 Mar 2011 18:53:05 +0100 hoelzl generalized Caratheodory from algebra to ring_of_sets
Tue, 22 Mar 2011 16:44:57 +0100 hoelzl add ring_of_sets and subset_class as basis for algebra
Tue, 22 Mar 2011 19:04:32 +0100 blanchet added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
Tue, 22 Mar 2011 18:38:29 +0100 blanchet added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
Tue, 22 Mar 2011 18:27:47 +0100 blanchet remove lie from documentation
Tue, 22 Mar 2011 17:20:54 +0100 blanchet let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
Tue, 22 Mar 2011 17:20:53 +0100 blanchet make Minimizer honor "verbose" and "debug" options better
Tue, 22 Mar 2011 12:49:07 +0100 nipkow fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
Mon, 21 Mar 2011 21:10:29 +0100 krauss moved some configurations to AFP, and fixed others
Tue, 22 Mar 2011 20:44:47 +0100 wenzelm more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
Tue, 22 Mar 2011 18:03:28 +0100 wenzelm enable inner syntax source positions by default (controlled via configuration option);
Tue, 22 Mar 2011 17:51:15 +0100 wenzelm binder_tr: more informative exception;
Tue, 22 Mar 2011 16:39:34 +0100 wenzelm Hoare syntax: strip positions where they crash translation functions;
Tue, 22 Mar 2011 16:15:50 +0100 wenzelm update_name_tr: more precise handling of explicit constraints, including positions;
Tue, 22 Mar 2011 15:32:47 +0100 wenzelm statespace syntax: strip positions -- type constraints are unexpected here;
Tue, 22 Mar 2011 14:45:48 +0100 wenzelm let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
Tue, 22 Mar 2011 14:22:40 +0100 wenzelm datatype case_tr: strip positions -- type constraints are unexpected despite the "any" category in "case_syn";
Tue, 22 Mar 2011 13:55:39 +0100 wenzelm tuned indendation and parentheses;
Tue, 22 Mar 2011 13:32:20 +0100 wenzelm support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
Tue, 22 Mar 2011 11:14:33 +0100 wenzelm pretty_string: proper handling of negative max_len;
Mon, 21 Mar 2011 23:38:32 +0100 wenzelm added Lexicon.encode_position, Lexicon.decode_position;
Mon, 21 Mar 2011 21:16:39 +0100 wenzelm tuned;
Mon, 21 Mar 2011 21:05:08 +0100 wenzelm tuned;
Mon, 21 Mar 2011 20:56:44 +0100 wenzelm clarified Syn_Trans.parsetree_to_ast and Syn_Trans.ast_to_term;
Mon, 21 Mar 2011 20:15:03 +0100 wenzelm tuned;
Mon, 21 Mar 2011 17:14:52 +0100 wenzelm merged
Mon, 21 Mar 2011 16:24:52 +0100 krauss added judgement day configurations
Mon, 21 Mar 2011 16:38:28 +0100 wenzelm another attempt to exec ISABELLE_GHC robustly (cf. d8c3b26b3da4, 994d088fbfbc);
Mon, 21 Mar 2011 14:46:59 +0100 krauss fixed perl error
Mon, 21 Mar 2011 14:37:10 +0100 krauss eliminated unnecessary generated ROOT.ML
Mon, 21 Mar 2011 14:25:59 +0100 krauss more precise dependencies
Mon, 21 Mar 2011 12:43:26 +0100 krauss small test case for main mirabelle functionality, which easily breaks without noticing
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip