Mercurial Mercurial > repos > isabelle / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -1920 +1920 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
Tue, 08 May 2012 14:31:03 +0200 bulwahn specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer changeset | files
Mon, 07 May 2012 14:50:49 +0200 blanchet prevent spurious timeouts changeset | files
Mon, 07 May 2012 12:20:55 +0200 blanchet added "try0" tool to Mirabelle changeset | files
Mon, 07 May 2012 12:20:55 +0200 blanchet use latest E (1.5) changeset | files
Fri, 04 May 2012 17:12:37 +0200 huffman lifting package produces abs_eq_iff rules for total quotients changeset | files
Fri, 04 May 2012 11:08:31 +0200 bulwahn using the new transfer method to obtain abstract properties of RBT trees changeset | files
Wed, 02 May 2012 22:05:59 +0200 wenzelm back to post-release mode -- after fork point; changeset | files
Wed, 23 May 2012 11:53:17 +0200 wenzelm removed obsolete RC tags; changeset | files
Tue, 22 May 2012 19:02:17 +0200 wenzelm Added tag Isabelle2012 for changeset 21c42b095c84 changeset | files
Sun, 20 May 2012 11:34:33 +0200 wenzelm try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09); Isabelle2012 changeset | files
Thu, 17 May 2012 16:04:39 +0200 wenzelm Added tag Isabelle2012-RC3 for changeset ed5f56b8f90a changeset | files
Thu, 17 May 2012 15:58:57 +0200 wenzelm some message; changeset | files
Thu, 17 May 2012 15:23:00 +0200 wenzelm tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph; changeset | files
Fri, 11 May 2012 13:41:30 +0200 berghofe Fixed disambiguation of names (cf. 5759ecd5c905) changeset | files
Thu, 10 May 2012 22:51:44 +0200 wenzelm merged changeset | files
Thu, 10 May 2012 22:49:12 +0200 wenzelm file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation; changeset | files
Thu, 10 May 2012 21:35:04 +0200 wenzelm prefer absolute paths, to allow launching from a different context (e.g. via file associations); changeset | files
Thu, 10 May 2012 20:49:30 +0200 wenzelm tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE"; changeset | files
Wed, 09 May 2012 16:46:12 +0200 wenzelm allow spaces in target directory; changeset | files
Mon, 07 May 2012 21:38:12 +0200 wenzelm Added tag Isabelle2012-RC2 for changeset 1636ff4c6243 changeset | files
Mon, 07 May 2012 20:35:53 +0200 wenzelm init Cygwin after unpacking; changeset | files
Sun, 06 May 2012 13:58:05 +0200 wenzelm tuned proofs; changeset | files
Sun, 06 May 2012 13:22:37 +0200 wenzelm more accurate ROOT.ML; changeset | files
Sun, 06 May 2012 11:52:33 +0200 wenzelm prefer http://isabelle.in.tum.de/library alias, which is available at TUM only; changeset | files
Sat, 05 May 2012 18:21:55 +0200 wenzelm some highlights of Isabelle2012; changeset | files
Fri, 04 May 2012 17:14:42 +0200 wenzelm refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on Cygwin and appears to be redundant anyway (no extra output produced within pipe); changeset | files
Fri, 04 May 2012 15:58:27 +0200 wenzelm some attempts to make critical errors fit on screen; changeset | files
Thu, 03 May 2012 22:07:29 +0200 wenzelm more NEWS; changeset | files
Thu, 03 May 2012 13:17:15 +0200 wenzelm backout 9579464d00f9 to avoid odd crash of polyml-5.2.1 (according to Jasmin, this change is not essential for now); changeset | files
Wed, 02 May 2012 22:40:28 +0200 wenzelm Added tag Isabelle2012-RC1 for changeset ec5d54029664 changeset | files
Wed, 02 May 2012 22:37:50 +0200 wenzelm clarified; changeset | files
Wed, 02 May 2012 21:55:13 +0200 wenzelm makedist for release; changeset | files
Wed, 02 May 2012 21:23:14 +0200 wenzelm merged changeset | files
Wed, 02 May 2012 21:21:51 +0200 wenzelm more contributors; changeset | files
Wed, 02 May 2012 21:15:38 +0200 wenzelm tuned latex sources; changeset | files
Wed, 02 May 2012 21:15:15 +0200 wenzelm more CHECKLIST; changeset | files
Wed, 02 May 2012 20:57:59 +0200 wenzelm save 90MB by removing foreign binaries -- multi-platform installations are unlikely on Windows; changeset | files
Wed, 02 May 2012 20:43:57 +0200 wenzelm some re-ordering; changeset | files
Wed, 02 May 2012 20:31:15 +0200 wenzelm some re-ordering; changeset | files
Wed, 02 May 2012 20:15:31 +0200 wenzelm tuned spelling; changeset | files
Wed, 02 May 2012 19:02:16 +0200 kuncar resolved maxidx bug changeset | files
Wed, 02 May 2012 18:26:10 +0200 kuncar documentation of the Lifting package on the ML level & tuned changeset | files
Wed, 02 May 2012 17:23:41 +0200 huffman edit NEWS items for transfer/lifting changeset | files
Wed, 02 May 2012 16:56:25 +0200 wenzelm avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube); changeset | files
Wed, 02 May 2012 16:04:07 +0200 wenzelm accomodate scala-2.10.0-M3 with its extra jar; changeset | files
Wed, 02 May 2012 13:09:26 +0200 wenzelm more robust wrt. spaces in directory names; changeset | files
Wed, 02 May 2012 11:47:45 +0200 wenzelm updated headers; changeset | files
Wed, 02 May 2012 11:45:00 +0200 wenzelm back to "Tools" in conformance with toplevel Isabelle layout (cf. 3fabf352243e, 15f4309bb9eb); changeset | files
Mon, 30 Apr 2012 21:59:10 +0200 blanchet export more symbols changeset | files
Mon, 30 Apr 2012 14:50:17 +0200 bulwahn merged changeset | files
Mon, 30 Apr 2012 13:48:30 +0200 bulwahn adding configuration to pass options to the ghc call in quickcheck[narrowing] changeset | files
Mon, 30 Apr 2012 22:18:39 +1000 Gerwin Klein provide [[record_codegen]] option for skipping codegen setup for records changeset | files
Mon, 30 Apr 2012 12:14:53 +0200 bulwahn making sorted_list_of_set executable changeset | files
Mon, 30 Apr 2012 12:14:51 +0200 bulwahn removing obsolete setup for sets now that sets are executable changeset | files
Mon, 30 Apr 2012 10:08:00 +0200 huffman update references in HOLCF README changeset | files
Sun, 29 Apr 2012 23:08:27 +0200 wenzelm basic setup for self-extracting 7zip installer; changeset | files
Sun, 29 Apr 2012 20:53:55 +0200 krauss merged changeset | files
Sun, 29 Apr 2012 20:39:34 +0200 krauss added test case for dependency graph (cf. 2d48bf79b725) changeset | files
Sun, 29 Apr 2012 01:17:25 +0200 krauss dependency graphs: fixed direction of edges changeset | files
Sun, 29 Apr 2012 20:42:09 +0200 wenzelm more CHECKLIST; changeset | files
Sun, 29 Apr 2012 19:03:57 +0200 wenzelm more windows-friendly presentation of main text files; changeset | files
Sun, 29 Apr 2012 11:44:33 +0200 blanchet split into demo and competitive version changeset | files
Sun, 29 Apr 2012 11:44:33 +0200 blanchet Sledgehammer can do it changeset | files
Sun, 29 Apr 2012 09:25:54 +0200 haftmann compact nat literals changeset | files
Sat, 28 Apr 2012 18:09:50 +0200 wenzelm some re-ordering; changeset | files
Sat, 28 Apr 2012 18:05:19 +0200 wenzelm some coverage of isabelle env; changeset | files
Sat, 28 Apr 2012 17:54:50 +0200 wenzelm updated system manual for release; changeset | files
Sat, 28 Apr 2012 17:53:12 +0200 wenzelm tuned; changeset | files
Sat, 28 Apr 2012 17:50:42 +0200 wenzelm some coverage of Isabelle/Scala tools; changeset | files
Sat, 28 Apr 2012 17:05:31 +0200 wenzelm some coverage of Isabelle/jEdit; changeset | files
Sat, 28 Apr 2012 16:44:32 +0200 wenzelm some manual updates; changeset | files
Sat, 28 Apr 2012 16:06:30 +0200 wenzelm some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x; changeset | files
Sat, 28 Apr 2012 11:24:20 +0200 huffman add isar-ref documentation for transfer package changeset | files
Sat, 28 Apr 2012 10:03:46 +0200 haftmann less confusion in NEWS changeset | files
Sat, 28 Apr 2012 09:55:01 +0200 haftmann rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly changeset | files
Sat, 28 Apr 2012 07:38:22 +0200 nipkow renamed Semi to Seq changeset | files
Fri, 27 Apr 2012 23:17:58 +0200 wenzelm merged changeset | files
Fri, 27 Apr 2012 22:58:29 +0200 wenzelm prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos; changeset | files
Fri, 27 Apr 2012 22:47:30 +0200 wenzelm clarified signature; changeset | files
Fri, 27 Apr 2012 21:47:47 +0200 wenzelm avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich; changeset | files
Fri, 27 Apr 2012 21:44:44 +0200 wenzelm made Context_Position independent from Config; changeset | files
Fri, 27 Apr 2012 22:36:27 +0200 blanchet use Nitpick as an oracle for finite problems changeset | files
Fri, 27 Apr 2012 22:36:27 +0200 blanchet add extensionality to first-order provers changeset | files
Fri, 27 Apr 2012 22:36:27 +0200 blanchet avoid duplicate helpers changeset | files
Fri, 27 Apr 2012 21:24:30 +0200 wenzelm mention tools and packages earlier; changeset | files
Fri, 27 Apr 2012 21:17:35 +0200 wenzelm tuned; changeset | files
Fri, 27 Apr 2012 21:13:55 +0200 wenzelm tuned; changeset | files
Fri, 27 Apr 2012 21:02:34 +0200 wenzelm tuned; changeset | files
Fri, 27 Apr 2012 20:57:40 +0200 wenzelm tuned; changeset | files
Fri, 27 Apr 2012 20:27:40 +0200 wenzelm merged changeset | files
Fri, 27 Apr 2012 17:14:13 +0200 huffman allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing changeset | files
Fri, 27 Apr 2012 17:06:36 +0200 kuncar documentation for the Lifting package in Isar-ref changeset | files
Fri, 27 Apr 2012 20:25:55 +0200 wenzelm added darwin targets; changeset | files
Fri, 27 Apr 2012 20:24:35 +0200 wenzelm chmod -x; changeset | files
Fri, 27 Apr 2012 20:10:09 +0200 wenzelm multi-platform build script and component settings; changeset | files
Fri, 27 Apr 2012 19:54:05 +0200 wenzelm print errors on stderr; changeset | files
Fri, 27 Apr 2012 19:50:32 +0200 wenzelm general exec_process -- nothing specific to Cygwin; changeset | files
Fri, 27 Apr 2012 19:31:03 +0200 wenzelm more direct exec with synchronous exit code; changeset | files
Fri, 27 Apr 2012 15:59:50 +0200 wenzelm some updates on classic README, reduce the impression that there is much to install manually; changeset | files
Fri, 27 Apr 2012 15:24:37 +0200 blanchet thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) changeset | files
Fri, 27 Apr 2012 15:24:37 +0200 blanchet move LEO-II closer to the top, for testing changeset | files
Fri, 27 Apr 2012 15:24:37 +0200 blanchet get rid of old CASC setup and move the arithmetic part to a new theory changeset | files
Fri, 27 Apr 2012 15:24:37 +0200 blanchet smaller batches, to play safe changeset | files
Fri, 27 Apr 2012 15:24:37 +0200 blanchet move file to where it belongs changeset | files
Fri, 27 Apr 2012 14:07:31 +0200 huffman implement transfer tactic with more scalable forward proof methods changeset | files
Fri, 27 Apr 2012 13:19:21 +0200 blanchet tuning changeset | files
Fri, 27 Apr 2012 13:18:55 +0200 blanchet tweak LEO-II setup changeset | files
Fri, 27 Apr 2012 12:16:10 +0200 blanchet eta-expand unapplied equalities in THF rather than using a proxy changeset | files
Fri, 27 Apr 2012 12:16:10 +0200 blanchet more tweaking of TPTP/CASC setup changeset | files
Thu, 26 Apr 2012 21:58:16 +0200 kuncar added a basic sanity check for quot_map changeset | files
Thu, 26 Apr 2012 20:22:39 +0200 wenzelm tuned comment; changeset | files
Thu, 26 Apr 2012 20:09:38 +0200 blanchet fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function changeset | files
Thu, 26 Apr 2012 19:44:18 +0200 wenzelm merged changeset | files
Thu, 26 Apr 2012 14:42:50 +0200 hoelzl add code equation for real_of_float changeset | files
Thu, 26 Apr 2012 14:11:13 +0200 kuncar tuned; don't generate abs code if quotient_type is used changeset | files
Thu, 26 Apr 2012 12:03:11 +0200 kuncar support Quotient map theorems with invariant parameters changeset | files
Thu, 26 Apr 2012 12:01:58 +0200 kuncar use a quot_map theorem attribute instead of the complicated map attribute changeset | files
Thu, 26 Apr 2012 01:05:06 +0200 blanchet further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical changeset | files
Thu, 26 Apr 2012 00:33:47 +0200 blanchet put Satallax first, at least for now (useful for experiments) changeset | files
Thu, 26 Apr 2012 00:33:23 +0200 blanchet tuning changeset | files
Thu, 26 Apr 2012 00:33:00 +0200 blanchet tuning changeset | files
Thu, 26 Apr 2012 00:29:46 +0200 blanchet tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p) changeset | files
Thu, 26 Apr 2012 00:28:06 +0200 blanchet tuning; no need for relevance filter changeset | files
Wed, 25 Apr 2012 23:39:19 +0200 blanchet tuning changeset | files
Wed, 25 Apr 2012 22:00:33 +0200 blanchet don't extensionalize formulas for higher-order provers -- Satallax in particular will only expand definitions of the form "constant = ..." changeset | files
Wed, 25 Apr 2012 22:00:33 +0200 blanchet don't use the native choice operator if the type encoding isn't higher-order changeset | files
Wed, 25 Apr 2012 22:00:33 +0200 blanchet tuning changeset | files
Wed, 25 Apr 2012 22:00:33 +0200 blanchet more work on TPTP Isabelle and Sledgehammer tactics changeset | files
Wed, 25 Apr 2012 22:00:33 +0200 blanchet more work on CASC setup changeset | files
Wed, 25 Apr 2012 22:53:35 +0200 wenzelm more direct bash process group invocation on Cygwin, bypassing extra sh.exe and perl.exe which tend to crash; changeset | files
Wed, 25 Apr 2012 20:08:33 +0200 wenzelm mingw is windows (still inactive); changeset | files
Wed, 25 Apr 2012 19:26:27 +0200 hoelzl add Caratheodories theorem for semi-rings of sets changeset | files
Wed, 25 Apr 2012 19:26:00 +0200 hoelzl moved lemmas to appropriate places changeset | files
Wed, 25 Apr 2012 17:15:10 +0200 wenzelm register polyml executables so that Cygwin rebaseall will see them; changeset | files
Wed, 25 Apr 2012 15:54:36 +0200 wenzelm merged changeset | files
Wed, 25 Apr 2012 15:44:26 +0200 wenzelm smarter PDF_VIEWER defaults, based on hints by Lars Noschinski; changeset | files
Wed, 25 Apr 2012 15:09:18 +0200 hoelzl equate positive Lebesgue integral and MV-Analysis' Gauge integral changeset | files
Wed, 25 Apr 2012 15:06:59 +0200 hoelzl correct lemma name changeset | files
Wed, 25 Apr 2012 14:33:21 +0200 blanchet tweak TPTP Nitpick's output changeset | files
Wed, 25 Apr 2012 14:33:21 +0200 blanchet remove too aggressive skolemization optimization (prevented discovery of a model in SYN994^1) changeset | files
Wed, 25 Apr 2012 14:33:21 +0200 blanchet improve precision (noticed on SEV296^5.thy) -- the exception for "bool" used to be necessary because of a hack where "opt" meant two different things changeset | files
Wed, 25 Apr 2012 14:33:21 +0200 blanchet output SZS status as early as possible changeset | files
Wed, 25 Apr 2012 14:28:13 +0200 hoelzl sorted lemma list in NEWS changeset | files
Wed, 25 Apr 2012 15:14:57 +0200 wenzelm merged changeset | files
Wed, 25 Apr 2012 15:13:40 +0200 wenzelm reactivated ListCellRenderer for Java 6 (cf. b9e2ed4b1579, 0ddac15782e4, de249b5ae6e2); changeset | files
Wed, 25 Apr 2012 15:13:03 +0200 wenzelm enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user; changeset | files
Wed, 25 Apr 2012 14:30:42 +0200 wenzelm updated README; changeset | files
Wed, 25 Apr 2012 14:29:15 +0200 wenzelm include generated application wrapper; changeset | files
Wed, 25 Apr 2012 14:24:27 +0200 wenzelm back to mature jdk1.6.0_31, to avoid issues like Sidekick TAB completion and generic ListCellRenderer; changeset | files
Wed, 25 Apr 2012 14:19:53 +0200 wenzelm ISABELLE_JDK_HOME is already provided by isatest shell environment; changeset | files
Wed, 25 Apr 2012 11:29:55 +0200 wenzelm added splash screen, to reduce confusion when waiting for main application to start up; changeset | files
Wed, 25 Apr 2012 10:59:06 +0200 wenzelm move polyml within Cygwin /usr/local to simplify its rebasing; changeset | files
Wed, 25 Apr 2012 10:24:41 +0200 wenzelm improved spelling; changeset | files
Wed, 25 Apr 2012 00:57:41 +0200 blanchet added "no_atp"s for extremely prolific, useless facts for ATPs changeset | files
Tue, 24 Apr 2012 23:22:40 +0200 wenzelm tuned; changeset | files
Tue, 24 Apr 2012 23:03:59 +0200 wenzelm merged changeset | files
Tue, 24 Apr 2012 20:55:09 +0200 blanchet made "split_last" more robust in the face of obscure low-level errors changeset | files
Tue, 24 Apr 2012 20:55:09 +0200 blanchet removed confusing error changeset | files
Tue, 24 Apr 2012 19:14:03 +0200 wenzelm some friendly message; changeset | files
Tue, 24 Apr 2012 16:09:17 +0200 wenzelm merged changeset | files
Tue, 24 Apr 2012 16:06:12 +0200 wenzelm merged changeset | files
Tue, 24 Apr 2012 14:13:04 +0100 sultana merged changeset | files
Tue, 24 Apr 2012 14:06:38 +0100 sultana merged changeset | files
Tue, 24 Apr 2012 13:59:29 +0100 sultana reversed Tools to Actions Mirabelle renaming; changeset | files
Tue, 24 Apr 2012 13:55:02 +0100 sultana tuned; changeset | files
Tue, 24 Apr 2012 13:56:13 +0200 blanchet reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path changeset | files
Tue, 24 Apr 2012 12:36:27 +0200 nipkow doc update changeset | files
Tue, 24 Apr 2012 15:56:09 +0200 wenzelm prefer evince over old xpdf -- NB: x86-cygwin bundles its own application; changeset | files
Tue, 24 Apr 2012 15:23:12 +0200 wenzelm cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat; changeset | files
Tue, 24 Apr 2012 15:07:49 +0200 wenzelm chmod -x; changeset | files
Tue, 24 Apr 2012 13:33:10 +0200 wenzelm augment Isabelle home directory more systematically; changeset | files
Tue, 24 Apr 2012 12:24:52 +0200 wenzelm Cygwin setup via the quasi-mirror isabelle.in.tum.de, which serves a fixed (downgraded) version; changeset | files
Tue, 24 Apr 2012 12:23:19 +0200 wenzelm prevent change of directory, by pretending we are the "Command Here" utility; changeset | files
Tue, 24 Apr 2012 11:07:50 +0200 nipkow typo changeset | files
Tue, 24 Apr 2012 10:44:04 +0200 nipkow the perennial doc problem of how to define lists a second time changeset | files
Tue, 24 Apr 2012 09:47:40 +0200 blanchet smoother handling of conjecture, so that its Skolem constants get displayed in countermodels changeset | files
Tue, 24 Apr 2012 09:47:40 +0200 blanchet updated doc changeset | files
Tue, 24 Apr 2012 09:47:40 +0200 blanchet add a timeout on the monotonicity check changeset | files
Tue, 24 Apr 2012 09:47:40 +0200 blanchet handle TPTP definitions as definitions in Nitpick rather than as axioms changeset | files
Tue, 24 Apr 2012 09:47:40 +0200 blanchet get rid of old parser, hopefully for good changeset | files
Tue, 24 Apr 2012 09:47:40 +0200 blanchet fix handling of atomizable conjectures without a top-level "Trueprop" (e.g. "x == (y::nat)") changeset | files
Tue, 24 Apr 2012 09:47:40 +0200 blanchet run Mirabelle in quick and dirty mode changeset | files
Tue, 24 Apr 2012 09:09:55 +0200 nipkow doc update changeset | files
Mon, 23 Apr 2012 23:55:06 +0200 wenzelm scrollable text; changeset | files
Mon, 23 Apr 2012 23:50:27 +0200 wenzelm bundle Cygwin-Terminal.bat; changeset | files
Mon, 23 Apr 2012 23:38:35 +0200 wenzelm basic Cygwin-Terminal for main Isabelle directory; changeset | files
Mon, 23 Apr 2012 22:26:22 +0200 wenzelm moved to ~isatest/.bashrc to accomodate AFP; changeset | files
Mon, 23 Apr 2012 22:22:57 +0200 wenzelm merged changeset | files
Mon, 23 Apr 2012 21:46:52 +0200 nipkow merged changeset | files
Mon, 23 Apr 2012 21:46:37 +0200 nipkow doc update changeset | files
Mon, 23 Apr 2012 21:31:52 +0200 krauss NEWS changeset | files
Mon, 23 Apr 2012 21:53:43 +0200 wenzelm typedef with implicit set definition is considered legacy; changeset | files
Mon, 23 Apr 2012 21:44:36 +0200 wenzelm more standard method setup; changeset | files
Mon, 23 Apr 2012 18:42:05 +0200 kuncar CONTRIBUTORS changeset | files
Mon, 23 Apr 2012 18:42:03 +0200 kuncar added useful Trueprop_conv changeset | files
Mon, 23 Apr 2012 17:18:18 +0200 kuncar move MRSL to a separate file changeset | files
Mon, 23 Apr 2012 16:30:43 +0200 wenzelm avoid conflict of Isabelle vs. Isabelle.exe on Cygwin; changeset | files
Mon, 23 Apr 2012 16:05:18 +0200 wenzelm more notes on Cygwin, notably for downgrading to 1.7.9 to avoid multi-threading instabilities starting with 1.7.10 early 2012; changeset | files
Mon, 23 Apr 2012 13:40:02 +0200 hoelzl CONTRIBUTORS changeset | files
Mon, 23 Apr 2012 12:14:35 +0200 hoelzl reworked Probability theory changeset | files
Mon, 23 Apr 2012 12:23:23 +0100 sultana updated test; changeset | files
Mon, 23 Apr 2012 12:23:23 +0100 sultana improved non-interpretation of constants and numbers; changeset | files
Mon, 23 Apr 2012 12:23:23 +0100 sultana improved interpreting conditionals; changeset | files
Mon, 23 Apr 2012 12:23:23 +0100 sultana disabled interpreting arithmetic; changeset | files
Mon, 23 Apr 2012 12:23:23 +0100 sultana improved handling of single-quoted names; changeset | files
Mon, 23 Apr 2012 12:23:23 +0100 sultana disabled exception packaging in tptp; changeset | files
Mon, 23 Apr 2012 12:23:23 +0100 sultana moved function for testing problem-name parsing; changeset | files
Mon, 23 Apr 2012 12:23:23 +0100 sultana removed redundant function; changeset | files
Sun, 22 Apr 2012 23:08:53 +0200 wenzelm bundle Isabelle.exe; changeset | files
Sun, 22 Apr 2012 21:32:35 +0200 huffman tuned precedence order of transfer rules changeset | files
Sun, 22 Apr 2012 22:02:52 +0200 wenzelm updated generated files; changeset | files
Sun, 22 Apr 2012 22:01:45 +0200 wenzelm updated const "relcomp"; changeset | files
Sun, 22 Apr 2012 21:47:32 +0200 wenzelm merged changeset | files
Sun, 22 Apr 2012 20:16:30 +0200 huffman add transfer rule for set difference changeset | files
Sun, 22 Apr 2012 21:43:57 +0200 wenzelm support Cygwin cold-start via Isabelle.exe, assuming layout of bundle; changeset | files
Sun, 22 Apr 2012 19:44:40 +0200 wenzelm merged changeset | files
Sun, 22 Apr 2012 19:18:26 +0200 huffman merged changeset | files
Sun, 22 Apr 2012 17:54:47 +0200 huffman adapt to changes in generated transfer rules (cf. 4483c004499a) changeset | files
Sun, 22 Apr 2012 16:53:24 +0200 huffman fix bug caused by misunderstanding of operator precedences (cf. cb44d09d9d22) changeset | files
Sun, 22 Apr 2012 19:04:30 +0200 wenzelm more robust handling of PATH vs PATH_JVM -- required for cold start of Cygwin from Windows (e.g. Isabelle.exe); changeset | files
Sun, 22 Apr 2012 16:33:41 +0200 wenzelm merged changeset | files
Sun, 22 Apr 2012 14:16:46 +0200 blanchet fixed typos changeset | files
Sun, 22 Apr 2012 14:16:46 +0200 blanchet tried harder to make SML/NJ happy changeset | files
Sun, 22 Apr 2012 14:16:46 +0200 blanchet added timeout argument to TPTP tools changeset | files
Sun, 22 Apr 2012 14:16:46 +0200 blanchet fix bug where "==" was used instead of "HOL.eq" changeset | files
Sun, 22 Apr 2012 14:16:46 +0200 blanchet more meaningful default value changeset | files
Sun, 22 Apr 2012 14:16:45 +0200 blanchet handle exception (needed to solve TPTP problem SEU880^5) changeset | files
Sun, 22 Apr 2012 16:32:26 +0200 wenzelm pretend jedit is up-to-date if this is not a repository -- avoid accidental build attempts after touching files etc.; changeset | files
Sun, 22 Apr 2012 16:08:10 +0200 wenzelm refer to isabelle.Main application wrapper; changeset | files
Sun, 22 Apr 2012 15:55:13 +0200 wenzelm display return code like Isabelle.app on Mac OS; changeset | files
Sun, 22 Apr 2012 15:50:29 +0200 wenzelm default Isabelle application wrapper -- JVM entry point for Isabelle.exe; changeset | files
Sun, 22 Apr 2012 15:19:46 +0200 wenzelm updated Isabelle.exe specification, assuming layout of bundle; changeset | files
Sun, 22 Apr 2012 14:30:18 +0200 wenzelm USER_HOME settings variable points to cross-platform user home directory; changeset | files
Sun, 22 Apr 2012 11:05:04 +0200 huffman new example theory for quotient/transfer changeset | files
Sat, 21 Apr 2012 21:38:08 +0200 huffman update NEWS for transfer/quotient changeset | files
Sat, 21 Apr 2012 20:52:33 +0200 huffman enable variant of transfer method that proves an implication instead of an equivalence changeset | files
Thu, 19 Apr 2012 19:36:24 +0200 haftmann moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator changeset | files
Sat, 21 Apr 2012 15:26:05 +0200 wenzelm merged changeset | files
Sat, 21 Apr 2012 13:54:29 +0200 huffman NEWS for transfer, lifting, and quotient changeset | files
Sat, 21 Apr 2012 13:49:31 +0200 huffman new example theory for transfer package changeset | files
Sat, 21 Apr 2012 14:53:04 +0200 wenzelm some builtin session timing; changeset | files
Sat, 21 Apr 2012 13:12:27 +0200 huffman move alternative definition lemmas into Lifting.thy; changeset | files
Sat, 21 Apr 2012 13:06:22 +0200 huffman tuned proofs changeset | files
Sat, 21 Apr 2012 11:21:23 +0200 huffman add transfer rule for List.set changeset | files
Sat, 21 Apr 2012 11:04:21 +0200 huffman remove duplicate of lemma id_transfer changeset | files
Sat, 21 Apr 2012 11:02:01 +0200 huffman added covariant relator set_rel, with transfer rules for set operations changeset | files
Sat, 21 Apr 2012 10:59:52 +0200 huffman renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator changeset | files
Sat, 21 Apr 2012 11:15:49 +0200 blanchet tried to make SML/NJ happy changeset | files
Sat, 21 Apr 2012 11:15:49 +0200 blanchet tuned "max_relevant" defaults for SMT solvers based on Judgment Day changeset | files
Sat, 21 Apr 2012 11:15:49 +0200 blanchet prepend PWD to relative paths changeset | files
Sat, 21 Apr 2012 11:15:49 +0200 blanchet reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures changeset | files
Sat, 21 Apr 2012 11:15:49 +0200 blanchet swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations changeset | files
Sat, 21 Apr 2012 07:33:47 +0200 huffman new transfer package rules and lifting setup for lists changeset | files
Sat, 21 Apr 2012 06:49:04 +0200 huffman strengthen rule list_all2_induct changeset | files
Fri, 20 Apr 2012 23:57:29 +0200 wenzelm more standard Theory_Data setup; changeset | files
Fri, 20 Apr 2012 23:34:03 +0200 wenzelm merged changeset | files
Fri, 20 Apr 2012 22:05:07 +0200 huffman add transfer rule for nat_case changeset | files
Fri, 20 Apr 2012 22:54:13 +0200 huffman uniform naming scheme for transfer rules changeset | files
Fri, 20 Apr 2012 22:49:40 +0200 huffman rename 'correspondence' method to 'transfer_prover' changeset | files
Fri, 20 Apr 2012 18:29:21 +0200 kuncar hide the invariant constant for relators: invariant_commute infrastracture changeset | files
Fri, 20 Apr 2012 23:16:46 +0200 wenzelm improved interleaving of start_execution vs. cancel_execution of the next update; changeset | files
Fri, 20 Apr 2012 23:15:44 +0200 wenzelm tuned proofs; changeset | files
Fri, 20 Apr 2012 22:48:48 +0200 wenzelm always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading; changeset | files
Fri, 20 Apr 2012 22:51:06 +0200 wenzelm tuned; changeset | files
Fri, 20 Apr 2012 20:29:44 +0200 wenzelm simplified internal actor protocol; changeset | files
Fri, 20 Apr 2012 20:21:22 +0200 wenzelm builtin timing for main operations; changeset | files
Fri, 20 Apr 2012 15:49:45 +0200 huffman add secondary transfer rule for universal quantifiers on non-bi-total relations changeset | files
Fri, 20 Apr 2012 15:34:33 +0200 huffman move definition of set_rel into Library/Quotient_Set.thy changeset | files
Fri, 20 Apr 2012 15:30:13 +0200 huffman add transfer rule for 'id' changeset | files
Fri, 20 Apr 2012 14:57:19 +0200 huffman add new transfer rules and setup for lifting package changeset | files
Fri, 20 Apr 2012 10:37:00 +0200 huffman setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq changeset | files
Fri, 20 Apr 2012 11:17:01 +0200 hoelzl NEWS changeset | files
Fri, 20 Apr 2012 11:14:39 +0200 hoelzl hide code generation facts in the Float theory, they are only exported for Approximation changeset | files
Fri, 20 Apr 2012 10:47:04 +0200 nipkow merged changeset | files
Fri, 20 Apr 2012 10:46:55 +0200 nipkow forgot to add file changeset | files
Fri, 20 Apr 2012 10:18:08 +0200 huffman make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules changeset | files
Thu, 19 Apr 2012 23:18:47 +0200 wenzelm merged changeset | files
Thu, 19 Apr 2012 22:21:15 +0200 hoelzl NEWS changeset | files
Thu, 19 Apr 2012 22:13:46 +0200 hoelzl transfer now handles Let changeset | files
Thu, 19 Apr 2012 20:19:24 +0200 nipkow merged changeset | files
Thu, 19 Apr 2012 20:19:13 +0200 nipkow added revised version of Abs_Int changeset | files
Thu, 19 Apr 2012 19:36:09 +0200 huffman add transfer rule for Let changeset | files
Thu, 19 Apr 2012 19:32:30 +0200 huffman add code lemmas for word operations changeset | files
Thu, 19 Apr 2012 19:18:47 +0200 haftmann tuned whitespace changeset | files
Thu, 19 Apr 2012 19:18:11 +0200 haftmann dropped dead code changeset | files
Thu, 19 Apr 2012 18:24:40 +0200 kuncar rename no_code to no_abs_code - more appropriate name changeset | files
Thu, 19 Apr 2012 17:31:34 +0200 kuncar use tnames for bound variables in rsp thms changeset | files
Thu, 19 Apr 2012 17:49:08 +0200 blanchet true delayed evaluation of "SPASS_VERSION" environment variable changeset | files
Thu, 19 Apr 2012 17:49:02 +0200 blanchet merged changeset | files
Thu, 19 Apr 2012 11:14:57 +0200 blanchet use latest Z3 changeset | files
Thu, 19 Apr 2012 17:32:35 +0200 nipkow merged changeset | files
Thu, 19 Apr 2012 17:32:30 +0200 nipkow reorganised IMP changeset | files
Thu, 19 Apr 2012 11:55:30 +0200 hoelzl use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems changeset | files
Wed, 18 Apr 2012 14:29:22 +0200 hoelzl use lifting to introduce floating point numbers changeset | files
Wed, 18 Apr 2012 14:29:21 +0200 hoelzl replace the float datatype by a type with unique representation changeset | files
Wed, 18 Apr 2012 14:29:20 +0200 hoelzl add lemmas to remove real conversions when compared to power of numerals changeset | files
Wed, 18 Apr 2012 14:29:20 +0200 hoelzl add simp rules to rewrite comparisons of 1 and real changeset | files
Wed, 18 Apr 2012 14:29:19 +0200 hoelzl add lemma to equate floor and div changeset | files
Wed, 18 Apr 2012 14:29:18 +0200 hoelzl add powr_inj changeset | files
Wed, 18 Apr 2012 14:29:17 +0200 hoelzl add lemmas to rewrite powr to power changeset | files
Wed, 18 Apr 2012 14:29:16 +0200 hoelzl add lemmas to compare log with 0 and 1 changeset | files
Wed, 18 Apr 2012 14:29:05 +0200 hoelzl add ceiling_diff_floor_le_1 changeset | files
Thu, 19 Apr 2012 23:15:58 +0200 wenzelm display Java 7 only code for now (cf. b9e2ed4b1579); changeset | files
Thu, 19 Apr 2012 21:53:24 +0200 wenzelm some sidekick options for more advanced completion; changeset | files
Thu, 19 Apr 2012 21:47:50 +0200 wenzelm custom ListCellRenderer with text area font ensures that symbols are displayed reliably; changeset | files
Thu, 19 Apr 2012 21:42:24 +0200 wenzelm tuned imports; changeset | files
Thu, 19 Apr 2012 19:54:48 +0200 wenzelm more robust wrt. exceptions; changeset | files
Thu, 19 Apr 2012 15:47:32 +0200 wenzelm accomodate digits within Isar command names, notably 'try0'; changeset | files
Thu, 19 Apr 2012 15:02:13 +0200 wenzelm more robust Sledgehammer in Prover IDE; changeset | files
Thu, 19 Apr 2012 14:59:17 +0200 wenzelm test with jdk-7u3 that is also bundled; changeset | files
Thu, 19 Apr 2012 12:28:10 +0200 kuncar create thm names correctly changeset | files
Thu, 19 Apr 2012 13:19:57 +0200 wenzelm updated components according to tentative bundle; changeset | files
Thu, 19 Apr 2012 13:15:06 +0200 wenzelm back to isatest with official polyml-5.4.1 (cf. ffa6e10df091); changeset | files
Thu, 19 Apr 2012 11:52:07 +0200 huffman use simpler method for preserving bound variable names in transfer tactic changeset | files
Thu, 19 Apr 2012 10:49:47 +0200 huffman tuned lemmas (v)image_id; changeset | files
Thu, 19 Apr 2012 11:10:03 +0200 blanchet use latest SPASS changeset | files
Thu, 19 Apr 2012 11:00:12 +0200 blanchet doc update changeset | files
Thu, 19 Apr 2012 10:16:51 +0200 haftmann dropped dead code; changeset | files
Thu, 19 Apr 2012 08:45:13 +0200 huffman generate abs_induct rules for quotient types changeset | files
Thu, 19 Apr 2012 09:58:54 +0200 haftmann tuned changeset | files
Thu, 19 Apr 2012 09:45:49 +0200 haftmann corrected Nbe.static_value: ignore cached compilations; changeset | files
Thu, 19 Apr 2012 09:31:36 +0200 haftmann tuned heading changeset | files
Wed, 18 Apr 2012 21:47:26 +0200 haftmann tuned name changeset | files
Thu, 19 Apr 2012 07:25:44 +0100 sultana improved threading of thy-values through interpret functions; changeset | files
Thu, 19 Apr 2012 07:25:41 +0100 sultana exceptions related to interpreting tptp problems now mention the relevant position in the tptp file; changeset | files
Wed, 18 Apr 2012 17:44:39 +0200 huffman add option to transfer method for specifying variables not to generalize over changeset | files
Tue, 17 Apr 2012 16:21:47 +1000 Thomas Sewell New tactic "word_bitwise" expands word equalities/inequalities into logic. changeset | files
Wed, 18 Apr 2012 23:57:44 +0200 kuncar setup_lifting: no_code switch and supoport for quotient theorems changeset | files
Wed, 18 Apr 2012 23:13:11 +0200 blanchet remove old TPTP CNF/FOF parser; always use Nik's new parser changeset | files
Wed, 18 Apr 2012 23:13:10 +0200 blanchet more standard SZS output changeset | files
Wed, 18 Apr 2012 22:40:25 +0200 blanchet Sledgehammer NEWS and CONTRIBUTORS changeset | files
Wed, 18 Apr 2012 22:40:25 +0200 blanchet tuned SZS status output changeset | files
Wed, 18 Apr 2012 22:40:25 +0200 blanchet update documentation (mostly based on feedback by Makarius) changeset | files
Wed, 18 Apr 2012 22:40:25 +0200 blanchet added SZS status wrappers in TPTP mode changeset | files
Wed, 18 Apr 2012 22:40:25 +0200 blanchet fixed Auto Nitpick's output changeset | files
Wed, 18 Apr 2012 22:39:35 +0200 blanchet phase out "$TPTP_PROBLEMS_PATH"; prefer "$TPTP" for consistency with CASC setup changeset | files
Wed, 18 Apr 2012 22:16:05 +0200 blanchet started integrating Nik's parser into TPTP command-line tools changeset | files
Wed, 18 Apr 2012 21:28:49 +0200 wenzelm merged changeset | files
Wed, 18 Apr 2012 21:11:50 +0200 haftmann tuned changeset | files
Wed, 18 Apr 2012 20:48:15 +0200 haftmann dropped errorneous NEWS entry changeset | files
Wed, 18 Apr 2012 21:06:12 +0200 wenzelm merged changeset | files
Wed, 18 Apr 2012 20:47:21 +0200 haftmann consolidated NEWS entries on fold changeset | files
Wed, 18 Apr 2012 20:45:48 +0200 haftmann grouped fold-related NEWS entries together changeset | files
Wed, 18 Apr 2012 20:40:52 +0200 haftmann grouped NEWS concerning relations together changeset | files
Wed, 18 Apr 2012 20:38:15 +0200 haftmann merged rename traces changeset | files
Wed, 18 Apr 2012 17:33:11 +0100 sultana fixed type interpretation; changeset | files
Wed, 18 Apr 2012 17:33:11 +0100 sultana more tptp testing support functions; changeset | files
Wed, 18 Apr 2012 18:24:16 +0200 nipkow tuned text, improved dependencies changeset | files
Wed, 18 Apr 2012 17:04:03 +0200 kuncar Lifting: generate more thms & note them & tuned changeset | files
Wed, 18 Apr 2012 15:48:32 +0200 huffman move constant 'Respects' into Lifting.thy; changeset | files
Wed, 18 Apr 2012 20:42:55 +0200 wenzelm more friendly sendback rendering, using green and "frisches Steingrau"; changeset | files
Wed, 18 Apr 2012 20:22:44 +0200 wenzelm more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace); changeset | files
Wed, 18 Apr 2012 18:31:48 +0200 wenzelm approximative file position for Pure entities; changeset | files
Wed, 18 Apr 2012 17:32:34 +0200 wenzelm render last ML_TYPING only -- relevant for inline antiquotations like @{term}; changeset | files
Wed, 18 Apr 2012 16:53:00 +0200 wenzelm flat presentation of collective markup; changeset | files
Wed, 18 Apr 2012 15:09:07 +0200 huffman add lemma Quotient_abs_induct changeset | files
Wed, 18 Apr 2012 14:59:04 +0200 huffman more usage of context blocks changeset | files
Wed, 18 Apr 2012 14:34:25 +0200 huffman use context block changeset | files
Wed, 18 Apr 2012 12:15:20 +0200 huffman lifting_setup generates transfer rule for rep of typedefs changeset | files
Wed, 18 Apr 2012 10:52:49 +0200 huffman use context block to organize typedef lifting theorems changeset | files
Wed, 18 Apr 2012 10:53:28 +0200 blanchet avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files changeset | files
Wed, 18 Apr 2012 10:53:28 +0200 blanchet compile changeset | files
Wed, 18 Apr 2012 10:53:28 +0200 blanchet get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run) changeset | files
Wed, 18 Apr 2012 10:53:27 +0200 blanchet doc update changeset | files
Wed, 18 Apr 2012 10:53:27 +0200 blanchet display more messages, now that more provers are run by default changeset | files
Tue, 17 Apr 2012 23:22:40 +0100 sultana added testing of tptp problem names; changeset | files
Tue, 17 Apr 2012 23:22:40 +0100 sultana tidied exception-handling relating to tptp problem names; changeset | files
Tue, 17 Apr 2012 23:22:40 +0100 sultana updated TPTP's ROOT.ML to include TPTP_Interpret; changeset | files
Tue, 17 Apr 2012 23:24:46 +0200 wenzelm retain ISABELLE_HOME_WINDOWS which is useful for jEdit to fold file names symbolically, but without DOS expansion that causes problems with Cygwin/Posix roundtrip (cf. 5a7903ba2dac); changeset | files
Tue, 17 Apr 2012 22:26:36 +0200 wenzelm updated to scala-2.9.2; changeset | files
Tue, 17 Apr 2012 14:00:09 +0200 huffman make transfer method more deterministic by using SOLVED' on some subgoals changeset | files
Tue, 17 Apr 2012 20:48:07 +0200 wenzelm accomodate ProofGeneral as Isabelle component, with adhoc version switch for Cygwin as before; changeset | files
Tue, 17 Apr 2012 19:16:13 +0200 kuncar tuned the setup of lifting; generate transfer rules for typedef and Quotient thms changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana improved exception-handling in tptp; changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana simplified interpretation of '$i'; changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana more cleaning of tptp tests; changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana improved tptp_graph robustness by relying on thy; changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana improved tptp interpretation test thy changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana tuned comments changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana improved handling of quoted names in tptp import changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana improved naming of 'distinct objects' in tptp import changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana reorganised tptp testing thys changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana enforced 'include' restrictions changeset | files
Tue, 17 Apr 2012 16:14:07 +0100 sultana tuned changeset | files
Tue, 17 Apr 2012 16:14:06 +0100 sultana split TPTP_Parser thy -- parser can rely on smaller image, whereas TPTP_Interpret requires HOL; changeset | files
Tue, 17 Apr 2012 16:48:37 +0200 wenzelm updated rel_comp ~> relcomp (cf. e1b761c216ac); changeset | files
Tue, 17 Apr 2012 15:25:43 +0200 blanchet merged changeset | files
Tue, 17 Apr 2012 13:54:31 +0200 blanchet more helpful error message changeset | files
Tue, 17 Apr 2012 13:54:31 +0200 blanchet avoid option introduced in E 1.2 when invoking older versions of E changeset | files
Tue, 17 Apr 2012 14:56:38 +0200 kuncar go back to the explicit compisition of quotient theorems changeset | files
Tue, 17 Apr 2012 11:03:08 +0200 huffman add theory data for relator identity rules; changeset | files
Tue, 17 Apr 2012 09:12:15 +0200 kuncar note the Quotient theorem in quotient_type changeset | files
Mon, 16 Apr 2012 20:50:43 +0200 kuncar leave Lifting prefix changeset | files
Mon, 16 Apr 2012 23:23:08 +0200 wenzelm more user aliases; changeset | files
Mon, 16 Apr 2012 23:07:40 +0200 wenzelm redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases; changeset | files
Mon, 16 Apr 2012 21:53:11 +0200 wenzelm updated and clarified OF/MRS; changeset | files
Mon, 16 Apr 2012 21:37:08 +0200 wenzelm document attribute "abs_def"; changeset | files
Mon, 16 Apr 2012 19:38:48 +0200 wenzelm repaired some damage caused by merging with version from 12 days ago (cf. 8c8f27864ed1); changeset | files
Mon, 16 Apr 2012 19:01:57 +0200 nipkow merged changeset | files
Wed, 04 Apr 2012 09:59:49 +0200 nipkow refined new tutorial announcement changeset | files
Mon, 16 Apr 2012 17:26:32 +0200 bulwahn merged changeset | files
Mon, 16 Apr 2012 17:22:51 +0200 Christian Sternagel duplicate "relpow" facts for "relpowp" (to emphasize that both worlds exist and obtain better search results with "find_theorems") changeset | files
Mon, 16 Apr 2012 17:20:32 +0200 wenzelm updated for release; changeset | files
Mon, 16 Apr 2012 15:09:47 +0200 wenzelm more precise handling of java failure, due to missing ISABELLE_JDK_HOME; changeset | files
Mon, 16 Apr 2012 11:24:57 +0200 huffman tuned some proofs; changeset | files
Sun, 15 Apr 2012 20:51:07 +0200 haftmann centralized enriched_type declaration, thanks to in-situ available Isar commands changeset | files
Sun, 15 Apr 2012 20:41:46 +0200 haftmann tuned whitespace changeset | files
Sun, 15 Apr 2012 18:55:45 +0200 huffman replace locale 'UFT' with new un-named context block feature; changeset | files
Sun, 15 Apr 2012 14:51:15 +0200 wenzelm more CONTRIBUTORS; changeset | files
Sun, 15 Apr 2012 14:50:09 +0200 wenzelm some coverage of bundled declarations; changeset | files
Sun, 15 Apr 2012 13:21:13 +0200 wenzelm more uniform outline; changeset | files
Sun, 15 Apr 2012 13:15:14 +0200 wenzelm some coverage of unnamed contexts, which can be nested within other targets; changeset | files
Sat, 14 Apr 2012 23:52:17 +0100 sultana gathered mirabelle_sledgehammer's hardcoded defaults changeset | files
Sat, 14 Apr 2012 23:52:17 +0100 sultana Mirabelle's 'usage' description relating to Sledgehammer now synchs with the ML code of the Mirabelle-Sledgehammer action changeset | files
Sat, 14 Apr 2012 23:52:17 +0100 sultana Mirabelle now gives usage info when no arguments given changeset | files
Sat, 14 Apr 2012 23:52:17 +0100 sultana switched from using sed to perl in mirabelle tool changeset | files
Sat, 14 Apr 2012 23:52:17 +0100 sultana renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description; changeset | files
Sat, 14 Apr 2012 23:34:18 +0200 wenzelm refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"; changeset | files
Sat, 14 Apr 2012 20:44:53 +0200 wenzelm merged; changeset | files
Sat, 14 Apr 2012 19:29:31 +0200 krauss removed HOL/ex/Set_Algebras -- outdated clone, obsolete as example changeset | files
Sat, 14 Apr 2012 15:08:59 +0100 sultana aligned tptp_graph dependencies to Isabelle conventions; changeset | files
Sat, 14 Apr 2012 20:10:10 +0200 wenzelm more ambitious isatest settings using polyml-svn (e.g. 1487); changeset | files
Sat, 14 Apr 2012 19:09:34 +0200 wenzelm use official TextArea.isCaretVisible and thus follow the "blink" flag; changeset | files
Sat, 14 Apr 2012 18:28:11 +0200 wenzelm display more memory; changeset | files
Sat, 14 Apr 2012 17:26:08 +0200 wenzelm keyword ";" is declared via prover (as "minor", not "diag"); changeset | files
Sat, 14 Apr 2012 17:15:57 +0200 wenzelm outermost SELECT_GOAL potentially improves performance; changeset | files
Sat, 14 Apr 2012 16:40:17 +0200 wenzelm report ISABELLE_HOME_WINDOWS; changeset | files
Sat, 14 Apr 2012 15:46:19 +0200 wenzelm chmod +x; changeset | files
Sat, 14 Apr 2012 14:36:36 +0200 wenzelm more robust invocation via ISABELLE_JDK_HOME and SCALA_HOME; changeset | files
Sat, 14 Apr 2012 13:05:59 +0200 wenzelm misc tuning for release; changeset | files
Sat, 14 Apr 2012 12:51:38 +0200 wenzelm revert changes of already published NEWS; changeset | files
Sat, 14 Apr 2012 12:46:45 +0200 wenzelm some updates for release; changeset | files
Sat, 14 Apr 2012 12:36:11 +0200 wenzelm more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation; changeset | files
Sat, 14 Apr 2012 11:46:35 +0200 wenzelm updated Scala/JVM versions; changeset | files
Fri, 13 Apr 2012 21:17:59 +0200 wenzelm include trailing comments in proper_command range; changeset | files
Fri, 13 Apr 2012 21:09:11 +0200 wenzelm minimal support for x86-mingw; changeset | files
Fri, 13 Apr 2012 19:44:15 +0200 wenzelm recognize MacOS on modern Java implementations, notably OpenJDK 1.7; changeset | files
Fri, 13 Apr 2012 19:42:48 +0200 wenzelm updated to Scala 2.9.2; changeset | files
Fri, 13 Apr 2012 14:00:26 +0200 wenzelm updated headers; changeset | files
Fri, 13 Apr 2012 13:59:35 +0200 wenzelm eliminated hard tabs; changeset | files
Fri, 13 Apr 2012 13:30:27 +0200 Andreas Lochbihler Automated merge with ssh://macbroy25.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle changeset | files
Fri, 13 Apr 2012 13:29:55 +0200 Andreas Lochbihler NEWS changeset | files
Fri, 13 Apr 2012 12:49:33 +0200 Andreas Lochbihler adapt to changes in RBT_Impl changeset | files
Fri, 13 Apr 2012 11:45:30 +0200 Andreas Lochbihler move RBT implementation into type class contexts changeset | files
Fri, 13 Apr 2012 12:09:25 +0200 wenzelm misc tuning; changeset | files
Fri, 13 Apr 2012 09:17:01 +0200 bulwahn NEWS changeset | files
Thu, 12 Apr 2012 23:51:36 +0200 krauss merged changeset | files
Thu, 12 Apr 2012 23:15:34 +0200 krauss distributivity of * over Un and UNION changeset | files
Thu, 12 Apr 2012 23:07:01 +0200 krauss Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and * changeset | files
Thu, 12 Apr 2012 22:55:11 +0200 krauss removed "setsum_set", now subsumed by generic setsum changeset | files
Thu, 12 Apr 2012 19:58:59 +0200 krauss backported Set_Algebras to use type classes (basically reverting b3e8d5ec721d from 2008) changeset | files
Thu, 12 Apr 2012 23:04:51 +0200 wenzelm tuned README; changeset | files
Thu, 12 Apr 2012 23:03:25 +0200 wenzelm direct scala toplevel tools to ISABELLE_JDK_HOME; changeset | files
Thu, 12 Apr 2012 22:59:00 +0200 wenzelm simplified component structure; changeset | files
Thu, 12 Apr 2012 19:48:23 +0200 wenzelm merged changeset | files
Thu, 12 Apr 2012 13:47:21 +0200 Andreas Lochbihler merged changeset | files
Thu, 12 Apr 2012 10:29:45 +0200 Andreas Lochbihler generalise case certificates to allow ignored parameters changeset | files
Thu, 12 Apr 2012 11:01:15 +0200 bulwahn merged changeset | files
Wed, 04 Apr 2012 15:15:48 +0900 griff manual merge changeset | files
Tue, 03 Apr 2012 17:45:06 +0900 griff dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q" changeset | files
Tue, 03 Apr 2012 17:26:30 +0900 griff renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow") changeset | files
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup; changeset | files
Thu, 12 Apr 2012 11:34:50 +0200 wenzelm more precise declaration of goal_tfrees in forked proof state; changeset | files
Thu, 12 Apr 2012 11:28:36 +0200 wenzelm partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt; changeset | files
Thu, 12 Apr 2012 10:13:33 +0200 bulwahn multiset operations are defined with lift_definitions; changeset | files
Thu, 12 Apr 2012 07:33:14 +0200 huffman remove outdated comment changeset | files
Wed, 11 Apr 2012 21:40:46 +0200 wenzelm rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers; changeset | files
Wed, 11 Apr 2012 20:42:28 +0200 wenzelm standardized ML aliases; changeset | files
Wed, 11 Apr 2012 15:02:48 +0200 wenzelm clarified proof_result: finish proof formally via head tr, not end_tr; changeset | files
Wed, 11 Apr 2012 14:20:51 +0200 wenzelm tuned; changeset | files
Wed, 11 Apr 2012 13:49:09 +0200 wenzelm more robust Future.fulfill wrt. duplicate assignment and interrupt; changeset | files
Wed, 11 Apr 2012 13:37:46 +0200 wenzelm tuned message; changeset | files
Wed, 11 Apr 2012 12:15:56 +0200 wenzelm always signal after cancel_group: passive tasks may have become active; changeset | files
Wed, 11 Apr 2012 11:44:21 +0200 wenzelm just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update; changeset | files
Tue, 10 Apr 2012 23:05:24 +0200 wenzelm merged changeset | files
Tue, 10 Apr 2012 16:10:50 +0100 Christian Urban moved lift_raw_const wrapper out of the Quotient-package into Nominal2 changeset | files
Tue, 10 Apr 2012 22:53:41 +0200 wenzelm misc tuning and simplification; changeset | files
Tue, 10 Apr 2012 21:31:05 +0200 wenzelm static relevance of proof via syntax keywords; changeset | files
Tue, 10 Apr 2012 20:42:17 +0200 wenzelm tuned future priorities: print 0, goal ~1, execute ~2; changeset | files
Tue, 10 Apr 2012 16:50:30 +0200 wenzelm updated for Poly/ML SVN 1476; changeset | files
Tue, 10 Apr 2012 11:42:15 +0200 wenzelm some coverage of HOL/TPTP; changeset | files
Tue, 10 Apr 2012 06:45:15 +0100 sultana added graph-conversion utility for TPTP files changeset | files
Tue, 10 Apr 2012 06:45:15 +0100 sultana moved non-interpret-specific code to different module changeset | files
Mon, 09 Apr 2012 23:06:14 +0200 wenzelm disable parallel proofs (again) -- still suffering from instabilites wrt. interrupts; changeset | files
Mon, 09 Apr 2012 21:29:47 +0200 wenzelm tuned proofs; changeset | files
Mon, 09 Apr 2012 20:57:23 +0200 wenzelm slightly faster default compilation of Isabelle/Scala; changeset | files
Mon, 09 Apr 2012 20:42:05 +0200 wenzelm more explicit last exec result; changeset | files
Mon, 09 Apr 2012 19:50:04 +0200 wenzelm dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result; changeset | files
Mon, 09 Apr 2012 17:38:39 +0200 wenzelm tuned; changeset | files
Mon, 09 Apr 2012 17:22:23 +0200 wenzelm simplified Future.cancel/cancel_group (again) -- running threads only; changeset | files
Mon, 09 Apr 2012 15:10:52 +0200 wenzelm added ML pretty-printing; changeset | files
Sat, 07 Apr 2012 20:35:01 +0200 wenzelm merged changeset | files
Sat, 07 Apr 2012 20:10:13 +0200 wenzelm merged changeset | files
Sat, 07 Apr 2012 20:24:39 +0200 haftmann explicit constructor Nat leaves nat_of as conversion changeset | files
Fri, 06 Apr 2012 19:23:51 +0200 haftmann abandoned almost redundant *_foldr lemmas changeset | files
Fri, 06 Apr 2012 19:18:00 +0200 haftmann tuned changeset | files
Fri, 06 Apr 2012 18:17:16 +0200 haftmann no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code changeset | files
Sat, 07 Apr 2012 19:59:09 +0200 wenzelm enable parallel proofs (cf. e8552cba702d), only affects packages so far; changeset | files
Sat, 07 Apr 2012 19:28:44 +0200 wenzelm added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel); changeset | files
Sat, 07 Apr 2012 18:08:29 +0200 wenzelm tuned proofs; changeset | files
Sat, 07 Apr 2012 17:55:35 +0200 wenzelm more robust update_perspective, e.g. required after reload of buffer that is not at start position; changeset | files
Sat, 07 Apr 2012 17:49:20 +0200 wenzelm tuned imports; changeset | files
Sat, 07 Apr 2012 17:48:47 +0200 wenzelm updated header keywords; changeset | files
Sat, 07 Apr 2012 16:59:27 +0200 wenzelm init message not bad; changeset | files
Sat, 07 Apr 2012 16:41:59 +0200 wenzelm explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; changeset | files
Fri, 06 Apr 2012 23:34:38 +0200 wenzelm discontinued obsolete last_execs (cf. cd3ab7625519); changeset | files
Fri, 06 Apr 2012 14:40:00 +0200 huffman remove now-unnecessary type annotations from lift_definition commands changeset | files
Fri, 06 Apr 2012 14:39:27 +0200 huffman more robust generation of quotient rules using tactics changeset | files
Fri, 06 Apr 2012 13:50:07 +0200 huffman merged changeset | files
Fri, 06 Apr 2012 10:37:46 +0200 huffman add function dest_Quotient changeset | files
Fri, 06 Apr 2012 13:10:45 +0200 wenzelm standardized alias; changeset | files
Fri, 06 Apr 2012 12:45:56 +0200 wenzelm fixed document; changeset | files
Fri, 06 Apr 2012 12:10:50 +0200 wenzelm merged changeset | files
Fri, 06 Apr 2012 09:35:47 +0200 huffman correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should changeset | files
Thu, 05 Apr 2012 23:22:54 +0200 kuncar detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr changeset | files
Thu, 05 Apr 2012 22:00:27 +0200 kuncar make Quotient_Def.lift_raw_const working again changeset | files
Thu, 05 Apr 2012 16:25:59 +0200 huffman use standard quotient lemmas to generate transfer rules changeset | files
Thu, 05 Apr 2012 15:59:25 +0200 huffman add transfer lemmas for quotients changeset | files
Thu, 05 Apr 2012 15:23:26 +0200 huffman define reflp directly, in the manner of symp and transp changeset | files
Thu, 05 Apr 2012 14:14:16 +0200 huffman set up and use lift_definition for word operations changeset | files
Thu, 05 Apr 2012 12:18:06 +0200 huffman lift_definition declares transfer_rule attribute changeset | files
Thu, 05 Apr 2012 10:48:46 +0200 huffman configure transfer method for 'a word -> int changeset | files
Thu, 05 Apr 2012 08:43:31 +0200 krauss added timestamps to logging of named thms changeset | files
Thu, 05 Apr 2012 08:13:40 +0200 huffman merged changeset | files
Wed, 04 Apr 2012 20:45:19 +0200 huffman merged changeset | files
Wed, 04 Apr 2012 16:48:39 +0200 huffman add lemmas for generating transfer rules for typedefs changeset | files
Thu, 05 Apr 2012 00:37:22 +0100 sultana tuned; changeset | files
Wed, 04 Apr 2012 21:57:39 +0100 sultana improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command; changeset | files
Wed, 04 Apr 2012 20:40:39 +0200 Cezary Kaliszyk merge changeset | files
Wed, 04 Apr 2012 20:10:21 +0200 Cezary Kaliszyk HOL/Import more precise map types changeset | files
Wed, 04 Apr 2012 20:09:56 +0200 Cezary Kaliszyk HOL/Import typed matches against Isabelle typedef result changeset | files
Wed, 04 Apr 2012 19:20:52 +0200 kuncar connect the Quotient package to the Lifting package changeset | files
Wed, 04 Apr 2012 17:51:12 +0200 kuncar support non-open typedefs; define cr_rel in terms of a rep function for typedefs changeset | files
Wed, 04 Apr 2012 16:29:17 +0100 sultana tuned; changeset | files
Wed, 04 Apr 2012 16:29:16 +0100 sultana added interpretation for formula conditional; changeset | files
Wed, 04 Apr 2012 16:29:16 +0100 sultana refactored tptp lex; changeset | files
Wed, 04 Apr 2012 16:29:16 +0100 sultana refactored tptp yacc to bring close to official spec; changeset | files
Wed, 04 Apr 2012 16:05:52 +0200 huffman transfer method generalizes over free variables in goal changeset | files
Wed, 04 Apr 2012 16:03:01 +0200 huffman add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer changeset | files
Wed, 04 Apr 2012 12:25:58 +0200 huffman update keywords file changeset | files
Wed, 04 Apr 2012 14:27:20 +0200 huffman merged changeset | files
Wed, 04 Apr 2012 11:50:08 +0200 huffman fix typos changeset | files
Wed, 04 Apr 2012 13:42:01 +0200 huffman lift_definition command generates transfer rule changeset | files
Wed, 04 Apr 2012 13:41:38 +0200 huffman prove_quot_theorem fixes types changeset | files
Wed, 04 Apr 2012 14:08:24 +0200 bulwahn documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS changeset | files
Wed, 04 Apr 2012 12:22:51 +0200 bulwahn added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck; changeset | files
Fri, 06 Apr 2012 12:02:24 +0200 wenzelm stop node execution at first unassigned exec; changeset | files
Fri, 06 Apr 2012 11:49:08 +0200 wenzelm discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution; changeset | files
Thu, 05 Apr 2012 22:33:52 +0200 wenzelm more scalable execute/update: avoid redundant traversal of invisible/finished nodes; changeset | files
Thu, 05 Apr 2012 14:34:54 +0200 wenzelm less ambitious memo_eval, since memo_result is still not robust here; changeset | files
Thu, 05 Apr 2012 14:14:51 +0200 wenzelm less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned; changeset | files
Thu, 05 Apr 2012 13:01:54 +0200 wenzelm more explicit memo_eval vs. memo_result, to enforce bottom-up execution; changeset | files
Thu, 05 Apr 2012 11:58:46 +0200 wenzelm Command.memo including physical interrupts (unlike Lazy.lazy); changeset | files
Thu, 05 Apr 2012 10:45:53 +0200 wenzelm tuned; changeset | files
Wed, 04 Apr 2012 21:03:30 +0200 wenzelm tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities; changeset | files
Wed, 04 Apr 2012 17:21:39 +0200 wenzelm proper signature constraint; changeset | files
Wed, 04 Apr 2012 17:14:19 +0200 wenzelm tuned comments; changeset | files
Wed, 04 Apr 2012 14:19:47 +0200 wenzelm separate module for prover command execution; changeset | files
Wed, 04 Apr 2012 14:00:47 +0200 wenzelm tuned; changeset | files
Wed, 04 Apr 2012 10:38:04 +0200 huffman fix typo in ML structure name changeset | files
Wed, 04 Apr 2012 11:15:54 +0200 wenzelm removed obsolete isar-overview manual; changeset | files
Wed, 04 Apr 2012 10:04:25 +0100 sultana dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret changeset | files
Wed, 04 Apr 2012 10:49:42 +0200 bulwahn merged changeset | files
Wed, 04 Apr 2012 10:17:54 +0200 bulwahn rudimentary handling of products in finitize_functions in Quickcheck-Narrowing changeset | files
Wed, 04 Apr 2012 10:17:08 +0200 bulwahn improved equality check for modes in predicate compiler changeset | files
Wed, 04 Apr 2012 09:00:10 +0200 huffman rename ML structure to avoid shadowing earlier name changeset | files
Wed, 04 Apr 2012 07:47:42 +0200 huffman add type annotations to make SML happy (cf. ec6187036495) changeset | files
Tue, 03 Apr 2012 23:49:24 +0200 huffman merged changeset | files
Tue, 03 Apr 2012 22:31:00 +0200 huffman new transfer proof method changeset | files
Tue, 03 Apr 2012 22:04:50 +0200 huffman renamed Tools/transfer.ML to Tools/legacy_transfer.ML changeset | files
Tue, 03 Apr 2012 21:39:28 +0200 wenzelm prefer prog-prove, suppress isar-overview; changeset | files
Tue, 03 Apr 2012 21:09:09 +0200 wenzelm merged changeset | files
Tue, 03 Apr 2012 20:41:13 +0200 wenzelm merged changeset | files
Tue, 03 Apr 2012 20:42:00 +0200 wenzelm formal integration of "prog-prove" manual; changeset | files
Tue, 03 Apr 2012 20:37:52 +0200 wenzelm prefer static dependencies; changeset | files
Tue, 03 Apr 2012 20:56:32 +0200 huffman merged changeset | files
Tue, 03 Apr 2012 15:15:00 +0200 huffman modernized obsolete old-style theory name with proper new-style underscore changeset | files
Tue, 03 Apr 2012 17:33:22 +0100 sultana removed use of CharVector in generated parser, to make SMLNJ happy changeset | files
Tue, 03 Apr 2012 20:24:00 +0200 wenzelm avoid duplicate PIDE markup; changeset | files
Tue, 03 Apr 2012 20:08:08 +0200 wenzelm less intrusive visibility; changeset | files
Tue, 03 Apr 2012 19:49:14 +0200 wenzelm more robust re-import wrt. non-HHF assumptions; changeset | files
Tue, 03 Apr 2012 19:33:46 +0200 wenzelm consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work; changeset | files
Tue, 03 Apr 2012 18:22:14 +0200 wenzelm close context elements via Expression.cert/read_declaration; changeset | files
Tue, 03 Apr 2012 17:48:16 +0200 wenzelm merged changeset | files
Tue, 03 Apr 2012 16:45:44 +0100 sultana added me to isatest email list changeset | files
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit changeset | files
Tue, 03 Apr 2012 14:09:37 +0200 huffman add floor/ceiling lemmas suggested by René Thiemann changeset | files
Tue, 03 Apr 2012 08:55:06 +0200 nipkow made sure that " is shown in tutorial text changeset | files
Mon, 02 Apr 2012 21:26:46 +0100 Christian Urban merged changeset | files
Mon, 02 Apr 2012 21:26:07 +0100 Christian Urban tuned proofs changeset | files
Mon, 02 Apr 2012 20:12:19 +0200 nipkow merged changeset | files
Mon, 02 Apr 2012 20:12:10 +0200 nipkow towards showing " in the tutorial changeset | files
Mon, 02 Apr 2012 18:12:53 +0100 Christian Urban tuned proof in order to avoid warning message changeset | files
Mon, 02 Apr 2012 16:07:24 +0200 huffman remove unnecessary qualifiers on names changeset | files
Mon, 02 Apr 2012 16:06:24 +0200 huffman add lemma Suc_1 changeset | files
Mon, 02 Apr 2012 14:09:27 +0200 berghofe merged changeset | files
Mon, 02 Apr 2012 13:58:59 +0200 berghofe Require "For" keyword to be followed by at least one whitespace, to avoid that changeset | files
Tue, 03 Apr 2012 17:21:33 +0200 wenzelm normalize defs (again, cf. 008b7858f3c0); changeset | files
Tue, 03 Apr 2012 16:53:32 +0200 wenzelm some context examples; changeset | files
Tue, 03 Apr 2012 16:51:01 +0200 wenzelm retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof; changeset | files
Tue, 03 Apr 2012 16:49:05 +0200 wenzelm another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix); changeset | files
Tue, 03 Apr 2012 16:27:32 +0200 wenzelm export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly); changeset | files
Tue, 03 Apr 2012 16:10:34 +0200 wenzelm better drop background syntax if entity depends on parameters; changeset | files
Tue, 03 Apr 2012 14:37:16 +0200 wenzelm more uniform abbrev vs. define; changeset | files
Tue, 03 Apr 2012 13:47:15 +0200 wenzelm tuned; changeset | files
Tue, 03 Apr 2012 11:28:21 +0200 wenzelm clarified generic_const vs. close_schematic_term; changeset | files
Tue, 03 Apr 2012 11:21:17 +0200 wenzelm tuned; changeset | files
Tue, 03 Apr 2012 10:59:20 +0200 wenzelm more uniform theory_abbrev with const_declaration; changeset | files
Tue, 03 Apr 2012 10:04:41 +0200 wenzelm avoid const_declaration in aux. context (cf. locale_foundation); changeset | files
Tue, 03 Apr 2012 09:47:20 +0200 wenzelm clarified background_foundation vs. theory_foundation (with const_declaration); changeset | files
Tue, 03 Apr 2012 09:41:16 +0200 wenzelm tuned; changeset | files
Mon, 02 Apr 2012 23:55:25 +0200 wenzelm more general standard_declaration; changeset | files
Mon, 02 Apr 2012 23:27:24 +0200 wenzelm better restore after close_target; changeset | files
Mon, 02 Apr 2012 21:52:03 +0200 wenzelm tuned; changeset | files
Mon, 02 Apr 2012 21:49:27 +0200 wenzelm clarified standard_declaration vs. theory_declaration; changeset | files
Mon, 02 Apr 2012 20:50:41 +0200 wenzelm smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax); changeset | files
Mon, 02 Apr 2012 20:12:17 +0200 wenzelm tuned; changeset | files
Mon, 02 Apr 2012 19:54:25 +0200 wenzelm tuned; changeset | files
Mon, 02 Apr 2012 19:47:21 +0200 wenzelm tuned signature; changeset | files
Mon, 02 Apr 2012 19:10:52 +0200 wenzelm misc tuning and simplification; changeset | files
Mon, 02 Apr 2012 17:00:32 +0200 wenzelm better restore to first target, not last target; changeset | files
Mon, 02 Apr 2012 16:35:09 +0200 wenzelm refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones); changeset | files
Mon, 02 Apr 2012 15:42:50 +0200 wenzelm more general Local_Theory.restore, allow any nesting level; changeset | files
Mon, 02 Apr 2012 13:47:00 +0200 nipkow new tutorial changeset | files
Mon, 02 Apr 2012 10:49:03 +0200 nipkow New manual Programming and Proving in Isabelle/HOL changeset | files
Mon, 02 Apr 2012 09:18:16 +0200 huffman add simp rules for dvd on negative numerals changeset | files
Sun, 01 Apr 2012 23:21:54 +0200 krauss merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49) changeset | files
Sun, 01 Apr 2012 23:09:36 +0200 krauss clarified terminology; added reference to bundle component changeset | files
Sun, 01 Apr 2012 22:55:06 +0200 krauss less modest NEWS; CONTRIBUTORS changeset | files
Sun, 01 Apr 2012 22:41:56 +0200 krauss renamed import session back to Import, conforming to directory name; NEWS changeset | files
Sun, 01 Apr 2012 23:07:15 +0200 wenzelm more precise IsaMakefile (eg. see HOL-Algebra); changeset | files
Sun, 01 Apr 2012 22:58:05 +0200 wenzelm more keywords; changeset | files
Sun, 01 Apr 2012 22:40:15 +0200 wenzelm merged changeset | files
Sun, 01 Apr 2012 22:14:59 +0200 krauss merged changeset | files
Sun, 01 Apr 2012 22:03:45 +0200 krauss removed old HOL4 import -- corresponding exporter is lost, code is broken, no users known, maintenance nightmare changeset | files
Sun, 01 Apr 2012 14:50:47 +0200 Cezary Kaliszyk Modernized HOL-Import for HOL Light changeset | files
Sun, 01 Apr 2012 22:26:28 +0200 wenzelm merged changeset | files
Sun, 01 Apr 2012 21:12:04 +0200 krauss adapted Mira configuration to dd04c8173bb2. changeset | files
Sun, 01 Apr 2012 16:09:58 +0200 huffman removed Nat_Numeral.thy, moving all theorems elsewhere changeset | files
Sun, 01 Apr 2012 22:02:14 +0200 wenzelm less brutal return from function, to allow caller to report error; changeset | files
Sun, 01 Apr 2012 21:46:45 +0200 wenzelm more general context command with auxiliary fixes/assumes etc.; changeset | files
Sun, 01 Apr 2012 21:45:25 +0200 wenzelm more precise type annotation (cf. 6523a21076a8); changeset | files
Sun, 01 Apr 2012 20:42:19 +0200 wenzelm nothing specific about named target; changeset | files
Sun, 01 Apr 2012 20:36:33 +0200 wenzelm clarified Generic_Target.notes: always perform Attrib.partial_evaluation; changeset | files
Sun, 01 Apr 2012 19:07:32 +0200 wenzelm added Attrib.global_notes/local_notes/generic_notes convenience; changeset | files
Sun, 01 Apr 2012 19:04:52 +0200 wenzelm simplified; changeset | files
Sun, 01 Apr 2012 18:01:19 +0200 wenzelm tuned signature; changeset | files
Sun, 01 Apr 2012 15:23:43 +0200 wenzelm clarified Named_Target.target_declaration: propagate through other levels as well; changeset | files
Sun, 01 Apr 2012 14:29:22 +0200 wenzelm Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom; changeset | files
Sun, 01 Apr 2012 09:12:03 +0200 huffman tuned proofs changeset | files
Sat, 31 Mar 2012 22:45:46 +0200 huffman merged changeset | files
Sat, 31 Mar 2012 20:09:24 +0200 huffman tuned proof changeset | files
Sat, 31 Mar 2012 19:10:58 +0200 huffman add lemma power_le_one changeset | files
Sat, 31 Mar 2012 19:38:41 +0200 wenzelm tuned; changeset | files
Sat, 31 Mar 2012 19:26:23 +0200 wenzelm tuned signature; changeset | files
Sat, 31 Mar 2012 19:09:59 +0200 wenzelm more direct Local_Defs.contract; changeset | files
Sat, 31 Mar 2012 15:29:49 +0200 wenzelm more precise Local_Defs.expand wrt. *local* prems only; changeset | files
Sat, 31 Mar 2012 15:21:35 +0200 wenzelm tuned comment; changeset | files
Fri, 30 Mar 2012 21:08:00 +0200 wenzelm more robust Scala 2.9.x interpreter invocation -- avoid separate interpreter thread and thus deadlock of Swing_Thread.now; changeset | files
Fri, 30 Mar 2012 19:36:41 +0200 wenzelm tuned; changeset | files
Fri, 30 Mar 2012 18:56:46 +0200 haftmann dropped empty files changeset | files
Fri, 30 Mar 2012 18:56:02 +0200 haftmann dropped now obsolete Cset theories changeset | files
Fri, 30 Mar 2012 17:25:34 +0200 wenzelm merged changeset | files
Fri, 30 Mar 2012 17:22:17 +0200 wenzelm tuned proofs, less guesswork; changeset | files
Fri, 30 Mar 2012 17:21:36 +0200 huffman merged changeset | files
Fri, 30 Mar 2012 16:44:23 +0200 huffman load Tools/numeral.ML in Num.thy changeset | files
Fri, 30 Mar 2012 16:43:07 +0200 huffman tuned proof changeset | files
Fri, 30 Mar 2012 15:56:12 +0200 huffman set up numeral reorient simproc in Num.thy changeset | files
Fri, 30 Mar 2012 15:43:30 +0200 huffman remove redundant simp rule changeset | files
Fri, 30 Mar 2012 15:24:24 +0200 huffman add simp rules for eve/odd on numerals changeset | files
Fri, 30 Mar 2012 14:27:29 +0200 huffman remove content-free theory ex/Arithmetic_Series_Complex.thy changeset | files
Fri, 30 Mar 2012 14:25:32 +0200 huffman rephrase lemmas about arithmetic series using numeral '2' changeset | files
Fri, 30 Mar 2012 14:00:18 +0200 huffman rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)' changeset | files
Fri, 30 Mar 2012 12:32:35 +0200 huffman replace lemmas eval_nat_numeral with a simpler reformulation changeset | files
Fri, 30 Mar 2012 12:02:23 +0200 huffman restate various simp rules for word operations using pred_numeral changeset | files
Fri, 30 Mar 2012 11:52:26 +0200 huffman new lemmas for simplifying subtraction on nat numerals changeset | files
Fri, 30 Mar 2012 11:16:35 +0200 huffman removed redundant nat-specific copies of theorems changeset | files
Fri, 30 Mar 2012 10:41:27 +0200 huffman move more theorems from Nat_Numeral.thy to Num.thy changeset | files
Fri, 30 Mar 2012 15:25:47 +0200 wenzelm "invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f); changeset | files
Fri, 30 Mar 2012 13:12:02 +0200 wenzelm more robust ISABELLE_JDK_HOME settings, based on exisiting JAVA_HOME provided by isatest shell environment (which depends a lot on the host); changeset | files
Fri, 30 Mar 2012 11:48:24 +0200 wenzelm more explicit isatest environment settings (from private .bashrc); changeset | files
Fri, 30 Mar 2012 09:55:03 +0200 huffman merged changeset | files
Fri, 30 Mar 2012 08:15:29 +0200 huffman fix search-and-replace errors changeset | files
Fri, 30 Mar 2012 08:04:28 +0200 huffman move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy changeset | files
Fri, 30 Mar 2012 09:08:29 +0200 huffman add constant pred_numeral k = numeral k - (1::nat); changeset | files
Fri, 30 Mar 2012 08:11:52 +0200 huffman move lemmas from Nat_Numeral.thy to Nat.thy changeset | files
Fri, 30 Mar 2012 08:10:28 +0200 huffman move lemmas from Nat_Numeral to Int.thy and Num.thy changeset | files
Fri, 30 Mar 2012 09:32:18 +0200 bulwahn merged changeset | files
Fri, 30 Mar 2012 08:44:01 +0200 bulwahn adding theory to prove completeness of the exhaustive generators changeset | files
Fri, 30 Mar 2012 08:19:31 +0200 bulwahn refine bindings in quickcheck_common: do not conceal and do not declare as simps changeset | files
Fri, 30 Mar 2012 08:19:29 +0200 bulwahn hiding fact not so aggressively changeset | files
Fri, 30 Mar 2012 09:04:29 +0200 haftmann power on predicate relations changeset | files
Fri, 30 Mar 2012 00:01:30 +0100 sultana made Mirabelle-SH's 'trivial' check optional; changeset | files
Thu, 29 Mar 2012 22:52:24 +0200 wenzelm merged changeset | files
Thu, 29 Mar 2012 22:43:50 +0200 wenzelm more specific notion of partiality (cf. Scala version); changeset | files
Thu, 29 Mar 2012 21:13:48 +0200 kuncar use qualified names for rsp and rep_eq theorems in quotient_def changeset | files
Thu, 29 Mar 2012 17:40:44 +0200 bulwahn announcing NEWS (cf. 446cfc760ccf) changeset | files
Thu, 29 Mar 2012 14:47:31 +0200 huffman remove obsolete simp rule for powers changeset | files
Thu, 29 Mar 2012 14:42:55 +0200 huffman remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd} changeset | files
Thu, 29 Mar 2012 14:39:05 +0200 huffman remove unneeded rewrite rules for powers of numerals changeset | files
Thu, 29 Mar 2012 14:29:36 +0200 huffman remove duplicate lemma Suc_numeral changeset | files
Thu, 29 Mar 2012 14:09:10 +0200 huffman move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy changeset | files
Thu, 29 Mar 2012 11:47:30 +0200 huffman bootstrap Num.thy before Power.thy; changeset | files
Thu, 29 Mar 2012 08:59:56 +0200 haftmann educated guess to include jdk changeset | files
Wed, 28 Mar 2012 17:57:23 +0200 nipkow improved robustness with new antiquoation by Makarius changeset | files
Wed, 28 Mar 2012 16:12:17 +0200 nipkow merged changeset | files
Wed, 28 Mar 2012 16:12:10 +0200 nipkow updates changeset | files
Wed, 28 Mar 2012 14:54:33 +0200 bulwahn updated documentation files (cf. c14fda8fee38) changeset | files
Wed, 28 Mar 2012 13:53:30 +0200 wenzelm clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME; changeset | files
Wed, 28 Mar 2012 13:38:56 +0200 wenzelm merged changeset | files
Wed, 28 Mar 2012 12:28:24 +0200 huffman removed references to obsolete theorems changeset | files
Wed, 28 Mar 2012 11:40:12 +0200 bulwahn merged changeset | files
Wed, 28 Mar 2012 10:44:04 +0200 bulwahn some tuning while reviewing the current state of the quotient_def package changeset | files
Wed, 28 Mar 2012 10:37:30 +0200 bulwahn improving spelling changeset | files
Wed, 28 Mar 2012 10:16:02 +0200 bulwahn changing more definitions to quotient_definition changeset | files
Wed, 28 Mar 2012 10:02:22 +0200 bulwahn removing now redundant impl_of theorems in DAList changeset | files
Wed, 28 Mar 2012 10:00:52 +0200 bulwahn using abstract code equations for proofs of code equations in Multiset changeset | files
Wed, 28 Mar 2012 12:08:08 +0200 wenzelm simplified statements and proofs; changeset | files
Wed, 28 Mar 2012 11:46:14 +0200 wenzelm tuned whitespace; changeset | files
Wed, 28 Mar 2012 11:17:32 +0200 wenzelm updated Sign.add_type, Name_Space.declare; changeset | files
Wed, 28 Mar 2012 11:04:39 +0200 wenzelm updated comments; changeset | files
Wed, 28 Mar 2012 08:25:51 +0200 huffman merged changeset | files
Tue, 27 Mar 2012 22:10:26 +0200 huffman remove unnecessary rules from the simpset changeset | files
Tue, 27 Mar 2012 21:58:41 +0200 huffman remove unused premises changeset | files
Tue, 27 Mar 2012 21:48:55 +0200 huffman remove duplicate lemmas changeset | files
Tue, 27 Mar 2012 21:48:26 +0200 huffman mark some duplicate lemmas for deletion changeset | files
Tue, 27 Mar 2012 20:19:23 +0200 huffman remove more redundant lemmas changeset | files
Tue, 27 Mar 2012 16:49:23 +0200 huffman tuned proofs changeset | files
Tue, 27 Mar 2012 19:21:05 +0200 huffman remove redundant lemmas changeset | files
Tue, 27 Mar 2012 16:04:51 +0200 huffman generalized lemma zpower_zmod changeset | files
Tue, 27 Mar 2012 15:53:48 +0200 huffman remove redundant lemma changeset | files
Tue, 27 Mar 2012 15:40:11 +0200 huffman remove redundant lemma changeset | files
Tue, 27 Mar 2012 15:34:36 +0200 huffman remove duplicate [algebra] declarations changeset | files
Tue, 27 Mar 2012 15:34:04 +0200 huffman generalize more div/mod lemmas changeset | files
Tue, 27 Mar 2012 15:27:49 +0200 huffman generalize some theorems about div/mod changeset | files
Wed, 28 Mar 2012 00:18:11 +0200 wenzelm updated to jedit-4.5.1; changeset | files
Tue, 27 Mar 2012 17:58:53 +0200 kuncar merged changeset | files
Tue, 27 Mar 2012 14:46:34 +0200 kuncar note a code eqn in quotient_def changeset | files
Tue, 27 Mar 2012 17:11:02 +0200 boehmes dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts) changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet fixed eta-extension of higher-order quantifiers in THF output changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet renamed "smt_fixed" to "smt_read_only_certificates" changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet tuning changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet tuning (in particular, Symtab instead of AList) changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet tweak slices, based on eval by Daniel Wand changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions) changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet print a hint changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet avoid DL changeset | files
Tue, 27 Mar 2012 16:59:13 +0300 blanchet TFF: declare free types as types changeset | files
Tue, 27 Mar 2012 15:34:04 +0200 bulwahn merged changeset | files
Tue, 27 Mar 2012 14:14:46 +0200 bulwahn association lists with distinct keys uses the quotient infrastructure to obtain code certificates; changeset | files
Tue, 27 Mar 2012 14:49:56 +0200 huffman remove redundant lemmas changeset | files
Tue, 27 Mar 2012 12:42:54 +0200 huffman move int::ring_div instance upward, simplify several proofs changeset | files
Tue, 27 Mar 2012 11:45:02 +0200 huffman rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names changeset | files
Tue, 27 Mar 2012 11:41:16 +0200 huffman extend definition of divmod_int_rel to handle denominator=0 case changeset | files
Tue, 27 Mar 2012 11:02:18 +0200 huffman tuned proofs changeset | files
Tue, 27 Mar 2012 10:34:12 +0200 huffman shorten a proof changeset | files
Tue, 27 Mar 2012 10:20:31 +0200 huffman simplify some proofs changeset | files
Tue, 27 Mar 2012 09:54:39 +0200 huffman rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc. changeset | files
Tue, 27 Mar 2012 09:44:56 +0200 huffman simplify some proofs changeset | files
Mon, 26 Mar 2012 21:03:30 +0200 wenzelm merged changeset | files
Mon, 26 Mar 2012 21:00:39 +0200 nipkow merged changeset | files
Mon, 26 Mar 2012 21:00:23 +0200 nipkow reverted to canonical name changeset | files
Mon, 26 Mar 2012 20:45:59 +0200 wenzelm merged changeset | files
Mon, 26 Mar 2012 20:11:27 +0200 huffman merged changeset | files
Mon, 26 Mar 2012 20:09:18 +0200 huffman revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda changeset | files
Mon, 26 Mar 2012 20:07:41 +0200 huffman merged changeset | files
Mon, 26 Mar 2012 20:07:29 +0200 huffman fix incorrect code_modulename declarations changeset | files
Mon, 26 Mar 2012 19:04:17 +0200 huffman code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda) changeset | files
Mon, 26 Mar 2012 19:03:27 +0200 huffman remove old-style semicolon changeset | files
Mon, 26 Mar 2012 20:09:52 +0200 nipkow merged changeset | files
Mon, 26 Mar 2012 18:54:41 +0200 nipkow Functions and lemmas by Christian Sternagel changeset | files
Mon, 26 Mar 2012 20:42:00 +0200 wenzelm more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit -- NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally; changeset | files
Mon, 26 Mar 2012 19:18:03 +0200 wenzelm disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d; changeset | files
Mon, 26 Mar 2012 18:32:22 +0200 kuncar tuned comment changeset | files
Mon, 26 Mar 2012 17:58:47 +0200 kuncar merged changeset | files
Mon, 26 Mar 2012 15:33:28 +0200 kuncar merged changeset | files
Mon, 26 Mar 2012 15:32:54 +0200 kuncar tuned proof - no smt call changeset | files
Mon, 26 Mar 2012 16:25:08 +0200 wenzelm more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function); changeset | files
Mon, 26 Mar 2012 15:38:09 +0200 wenzelm updated theory header syntax and related details; changeset | files
Sat, 24 Mar 2012 20:24:16 +0100 wenzelm ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE); changeset | files
Mon, 26 Mar 2012 11:15:41 +0200 wenzelm merged changeset | files
Mon, 26 Mar 2012 11:01:04 +0200 blanchet reintroduced broken proofs and regenerated certificates changeset | files
Mon, 26 Mar 2012 10:56:56 +0200 wenzelm merged, resolving trivial conflict; changeset | files
Mon, 26 Mar 2012 10:42:06 +0200 blanchet fixed Nitpick after numeral representation change (2a1953f0d20d) changeset | files
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS) changeset | files
Sat, 24 Mar 2012 16:27:04 +0100 kuncar merged changeset | files
Fri, 23 Mar 2012 22:00:17 +0100 kuncar use Thm.transfer for thms stored in generic context data storage changeset | files
Fri, 23 Mar 2012 18:23:47 +0100 kuncar hide invariant constant changeset | files
Sat, 24 Mar 2012 12:28:45 +0100 wenzelm explicit SMTP server (appears to be required after recent change of system configuration); changeset | files
Sat, 24 Mar 2012 12:22:29 +0100 wenzelm more isatest subscribers; changeset | files
Fri, 23 Mar 2012 16:16:35 +0000 paulson merged changeset | files
Fri, 23 Mar 2012 16:16:15 +0000 paulson proof tidying changeset | files
Mon, 16 Jan 2012 12:33:26 +0100 kuncar updated comment changeset | files
Fri, 23 Mar 2012 14:34:50 +0100 kuncar resolve invariant constant name clash changeset | files
Fri, 23 Mar 2012 14:29:29 +0100 kuncar update etc/isar-keywords.el changeset | files
Fri, 23 Mar 2012 14:26:09 +0100 kuncar fix example files changeset | files
Fri, 23 Mar 2012 14:25:31 +0100 kuncar generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem changeset | files
Fri, 23 Mar 2012 14:21:41 +0100 kuncar simplified code of generation of aggregate relations changeset | files
Fri, 23 Mar 2012 14:20:09 +0100 kuncar store the relational theorem for every relator changeset | files
Fri, 23 Mar 2012 14:18:43 +0100 kuncar store the quotient theorem for every quotient changeset | files
Fri, 23 Mar 2012 14:17:29 +0100 kuncar fix Quotient_Examples changeset | files
Fri, 23 Mar 2012 14:03:58 +0100 kuncar respectfulness theorem has to be proved if a new constant is lifted by quotient_definition changeset | files
Fri, 23 Mar 2012 12:03:59 +0100 bulwahn adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3 changeset | files
Fri, 23 Mar 2012 20:32:43 +0100 wenzelm tuned; changeset | files
Thu, 22 Mar 2012 21:43:26 +0100 wenzelm merged; changeset | files
Thu, 22 Mar 2012 18:54:39 +0100 haftmann fixed typo changeset | files
Thu, 22 Mar 2012 18:37:20 +0100 haftmann more instructive NEWS changeset | files
Thu, 22 Mar 2012 17:52:50 +0000 paulson more structured proofs changeset | files
Thu, 22 Mar 2012 16:41:22 +0000 paulson New Message changeset | files
Thu, 22 Mar 2012 10:10:02 +0100 berghofe No longer treat "title" as FDL keyword changeset | files
Thu, 22 Mar 2012 16:44:19 +0100 wenzelm tuned proofs; changeset | files
Thu, 22 Mar 2012 15:41:49 +0100 wenzelm uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters); changeset | files
Thu, 22 Mar 2012 11:11:51 +0100 wenzelm tuned; changeset | files
Thu, 22 Mar 2012 10:49:31 +0100 wenzelm synchronize syntax uniformly for target stack and aux. context; changeset | files
Thu, 22 Mar 2012 10:10:30 +0100 wenzelm tuned; changeset | files
Wed, 21 Mar 2012 23:41:22 +0100 wenzelm merged changeset | files
Wed, 21 Mar 2012 16:53:24 +0100 blanchet removed Satallax option, now that this is the default changeset | files
Wed, 21 Mar 2012 16:53:24 +0100 blanchet doc update changeset | files
Wed, 21 Mar 2012 16:53:24 +0100 blanchet improve "remote_satallax" by exploiting unsat core changeset | files
Wed, 21 Mar 2012 16:53:24 +0100 blanchet generate weights and precedences for predicates as well changeset | files
Wed, 21 Mar 2012 15:43:02 +0000 paulson refinements to constructibility changeset | files
Wed, 21 Mar 2012 13:05:40 +0000 paulson More structured proofs for infinite cardinalities changeset | files
Wed, 21 Mar 2012 23:41:58 +0100 wenzelm actually expose target context; changeset | files
Wed, 21 Mar 2012 23:26:35 +0100 wenzelm more explicit Toplevel.open_target/close_target; changeset | files
Wed, 21 Mar 2012 21:24:13 +0100 wenzelm tuned signature; changeset | files
Wed, 21 Mar 2012 21:06:31 +0100 wenzelm optional 'includes' element for long theorem statements; changeset | files
Wed, 21 Mar 2012 17:25:35 +0100 wenzelm basic support for nested contexts including bundles; changeset | files
Wed, 21 Mar 2012 17:16:39 +0100 wenzelm tuned messages; changeset | files
Wed, 21 Mar 2012 15:19:45 +0100 wenzelm basic support for nested local theory targets; changeset | files
Wed, 21 Mar 2012 13:54:33 +0100 wenzelm try apple.laf.useScreenMenuBar=false to make menus stay closer to the editor views they belong to -- potentially less confusing for jEdit newcomers; changeset | files
Wed, 21 Mar 2012 11:36:47 +0100 wenzelm improved isatest arguments for macbroy2; changeset | files
Wed, 21 Mar 2012 11:25:19 +0100 wenzelm clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2); changeset | files
Wed, 21 Mar 2012 11:00:34 +0100 wenzelm prefer explicitly qualified exception List.Empty; changeset | files
Tue, 20 Mar 2012 21:37:31 +0100 wenzelm merged changeset | files
Tue, 20 Mar 2012 21:34:42 +0100 wenzelm refined init_model: allow change of buffer name as caused by "Save as", for example; changeset | files
Tue, 20 Mar 2012 20:00:13 +0100 wenzelm basic support for bundled declarations; changeset | files
Tue, 20 Mar 2012 18:42:45 +0100 blanchet doc update changeset | files
Tue, 20 Mar 2012 18:42:45 +0100 blanchet made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release changeset | files
Tue, 20 Mar 2012 18:42:45 +0100 blanchet removed obsolete temporary hack changeset | files
Tue, 20 Mar 2012 18:42:45 +0100 blanchet tweaks changeset | files
Tue, 20 Mar 2012 17:20:33 +0000 paulson proof tidying changeset | files
Tue, 20 Mar 2012 18:01:34 +0100 wenzelm minimalistic support for remote URLs: no master dir here; changeset | files
Tue, 20 Mar 2012 13:53:09 +0100 blanchet optimized "metis" call changeset | files
Tue, 20 Mar 2012 13:53:09 +0100 blanchet added term_order option to Mirabelle changeset | files
Tue, 20 Mar 2012 13:53:09 +0100 blanchet take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them changeset | files
Tue, 20 Mar 2012 13:53:09 +0100 blanchet more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV") changeset | files
Tue, 20 Mar 2012 13:53:09 +0100 blanchet remove two options that were found to play hardly any role changeset | files
Tue, 20 Mar 2012 13:53:09 +0100 blanchet enable "metis_advisory_simp" by default changeset | files
Tue, 20 Mar 2012 13:02:07 +0100 wenzelm more stats; changeset | files
Tue, 20 Mar 2012 11:03:46 +0000 paulson merged changeset | files
Tue, 20 Mar 2012 11:03:25 +0000 paulson more structured proofs changeset | files
Tue, 20 Mar 2012 10:45:52 +0100 blanchet don't generate new SPASS constructs for old SPASS changeset | files
Tue, 20 Mar 2012 10:21:05 +0100 blanchet tune Metis example changeset | files
Tue, 20 Mar 2012 10:06:35 +0100 blanchet added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle") changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet continued implementation of term ordering attributes changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet added "dont_preplay" alias changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet document "dont_preplay" changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet tuning changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet implement term order attribute (for experiments) changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet tuning -- don't refer to old, internal version number (needlessly confusing now) changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet more weight attribute tuning changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0 changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet internal renamings changeset | files
Tue, 20 Mar 2012 00:44:30 +0100 blanchet renamed E weight attribute changeset | files
Mon, 19 Mar 2012 23:17:18 +0100 wenzelm tuned proofs; changeset | files
Mon, 19 Mar 2012 23:08:27 +0100 wenzelm explicit propagation of assignment event, even if changed command set is empty; changeset | files
Mon, 19 Mar 2012 21:52:09 +0100 wenzelm modernized axiomatizations; changeset | files
Mon, 19 Mar 2012 21:49:52 +0100 wenzelm modernized axiomatizations; changeset | files
Mon, 19 Mar 2012 21:25:15 +0100 wenzelm updated Misc_Legacy.freeze_thaw; changeset | files
Mon, 19 Mar 2012 21:16:19 +0100 wenzelm discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63); changeset | files
Mon, 19 Mar 2012 21:10:33 +0100 wenzelm moved some legacy stuff; changeset | files
Mon, 19 Mar 2012 20:32:57 +0100 wenzelm clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e); changeset | files
Mon, 19 Mar 2012 19:49:54 +0100 wenzelm merged changeset | files
Mon, 19 Mar 2012 15:20:00 +0000 paulson merged changeset | files
Mon, 19 Mar 2012 15:19:38 +0000 paulson More structured proofs for cardinalities changeset | files
Mon, 19 Mar 2012 10:52:48 +0000 paulson merged changeset | files
Fri, 16 Mar 2012 17:41:53 +0000 paulson more structured case and induction proofs changeset | files
Mon, 19 Mar 2012 12:43:46 +0100 blanchet better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete changeset | files
Mon, 19 Mar 2012 18:18:42 +0100 wenzelm allow keyword tags to be redefined, but not the command category; changeset | files
Mon, 19 Mar 2012 15:56:27 +0100 wenzelm further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe; changeset | files
Mon, 19 Mar 2012 14:59:31 +0100 wenzelm clarified command span classification: strict Command.is_command, permissive Command.name; changeset | files
Sun, 18 Mar 2012 22:09:00 +0100 wenzelm more robust bash interpolation; changeset | files
Sun, 18 Mar 2012 22:06:37 +0100 wenzelm more ambitious scalac options for makedist; changeset | files
Sun, 18 Mar 2012 21:52:50 +0100 wenzelm less noisy Isabelle/Scala build process; changeset | files
Sun, 18 Mar 2012 13:59:54 +0100 wenzelm comment; changeset | files
Sun, 18 Mar 2012 13:51:51 +0100 wenzelm tuned; changeset | files
Sun, 18 Mar 2012 13:37:11 +0100 wenzelm tuned; changeset | files
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); changeset | files
Sun, 18 Mar 2012 12:51:44 +0100 wenzelm tuned; changeset | files
Sun, 18 Mar 2012 10:28:31 +0100 wenzelm tuned structure; changeset | files
Sun, 18 Mar 2012 08:57:45 +0100 haftmann comments for uniformity changeset | files
Sat, 17 Mar 2012 23:55:03 +0100 wenzelm proper naming of simprocs according to actual target context; changeset | files
Sat, 17 Mar 2012 23:50:47 +0100 wenzelm amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4; changeset | files
Sat, 17 Mar 2012 22:46:19 +0100 wenzelm more precise syntax; changeset | files
Sat, 17 Mar 2012 17:58:40 +0100 wenzelm more antiquotations; changeset | files
Sat, 17 Mar 2012 17:44:29 +0100 wenzelm misc tuning to accomodate scala-2.10.0-M2; changeset | files
Sat, 17 Mar 2012 17:36:10 +0100 wenzelm include scala.xml as of scala-2.9.1.final/misc/scala-tool-support/jedit/modes/scala.xml -- seems to be missing in more recent distributions; changeset | files
Sat, 17 Mar 2012 16:13:41 +0100 wenzelm merged changeset | files
Sat, 17 Mar 2012 12:37:32 +0000 paulson merged changeset | files
Sat, 17 Mar 2012 12:36:11 +0000 paulson tidying and structured proofs changeset | files
Sat, 17 Mar 2012 16:07:03 +0100 wenzelm refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.; changeset | files
Sat, 17 Mar 2012 15:33:08 +0100 wenzelm tuned proofs; changeset | files
Sat, 17 Mar 2012 14:01:09 +0100 wenzelm simultaneous read_fields -- e.g. relevant for sort assignment; changeset | files
Sat, 17 Mar 2012 13:06:23 +0100 wenzelm added Syntax.read_typs; changeset | files
Sat, 17 Mar 2012 12:52:40 +0100 wenzelm renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP; changeset | files
Sat, 17 Mar 2012 12:26:19 +0100 wenzelm tuned message; changeset | files
Sat, 17 Mar 2012 12:21:15 +0100 wenzelm tuned proofs; changeset | files
Sat, 17 Mar 2012 12:00:11 +0100 wenzelm tuned proofs; changeset | files
Sat, 17 Mar 2012 11:59:59 +0100 wenzelm tuned exception; changeset | files
Sat, 17 Mar 2012 11:57:03 +0100 wenzelm merged; changeset | files
Sat, 17 Mar 2012 11:35:18 +0100 haftmann spelt out missing colemmas changeset | files
Sat, 17 Mar 2012 08:00:18 +0100 haftmann generalized INF_INT_eq, SUP_UN_eq changeset | files
Fri, 16 Mar 2012 22:26:55 +0100 haftmann tuned specifications changeset | files
Sat, 17 Mar 2012 11:23:14 +0100 wenzelm sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold; changeset | files
Sat, 17 Mar 2012 10:55:08 +0100 wenzelm tuned grouping -- merely indicate order of magnitude; changeset | files
Sat, 17 Mar 2012 10:54:15 +0100 wenzelm slightly more parallel find_theorems; changeset | files
Sat, 17 Mar 2012 09:51:18 +0100 wenzelm 'definition' no longer exports the foundational "raw_def"; changeset | files
Sat, 17 Mar 2012 00:17:30 +0100 wenzelm some attempts to fit source on screen; changeset | files
Fri, 16 Mar 2012 22:48:38 +0100 wenzelm eliminated odd 'finalconsts' / Theory.add_finals; changeset | files
Fri, 16 Mar 2012 22:31:19 +0100 wenzelm modernized axiomatization; changeset | files
Fri, 16 Mar 2012 22:22:05 +0100 wenzelm modernized axiomatization; changeset | files
Fri, 16 Mar 2012 21:59:19 +0100 wenzelm afford strict Args.type_name (cf. 29e88714ffe4); changeset | files
Fri, 16 Mar 2012 21:40:21 +0100 wenzelm check declared vs. defined commands at end of session; changeset | files
Fri, 16 Mar 2012 21:20:23 +0100 wenzelm more abstract heading level; changeset | files
Fri, 16 Mar 2012 20:45:47 +0100 wenzelm less redundant data; changeset | files
Fri, 16 Mar 2012 20:33:33 +0100 wenzelm uniform keyword names within ML/Scala -- produce elisp names via external conversion; changeset | files
Fri, 16 Mar 2012 18:21:22 +0100 wenzelm merged changeset | files
Fri, 16 Mar 2012 16:32:34 +0000 paulson ZF news changeset | files
Fri, 16 Mar 2012 16:29:51 +0000 paulson merged changeset | files
Fri, 16 Mar 2012 16:29:28 +0000 paulson Structured transfinite induction proofs changeset | files
Fri, 16 Mar 2012 15:51:53 +0100 huffman make more word theorems respect int/bin distinction changeset | files
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations; changeset | files
Fri, 16 Mar 2012 14:46:13 +0100 wenzelm refute_params are given in *this* theory; changeset | files
Fri, 16 Mar 2012 14:42:11 +0100 wenzelm defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined; changeset | files
Fri, 16 Mar 2012 13:05:30 +0100 wenzelm define keywords early when processing the theory header, before running the body commands; changeset | files
Fri, 16 Mar 2012 11:26:55 +0100 wenzelm clarified Keyword.is_keyword: union of minor and major; changeset | files
Thu, 15 Mar 2012 23:06:22 +0100 wenzelm Isabelle/jEdit supports user-defined Isar commands within the running session; changeset | files
Thu, 15 Mar 2012 22:21:28 +0100 wenzelm merged changeset | files
Thu, 15 Mar 2012 17:38:05 +0000 paulson beautification and structured proofs changeset | files
Thu, 15 Mar 2012 16:35:02 +0000 paulson replacing ":" by "\<in>" changeset | files
Thu, 15 Mar 2012 15:54:22 +0000 paulson Rewrote some induction proofs to be structured changeset | files
Thu, 15 Mar 2012 22:20:07 +0100 wenzelm more precise TPTP keywords and dependencies; changeset | files
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure; changeset | files
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser; changeset | files
Thu, 15 Mar 2012 19:48:19 +0100 wenzelm added ML antiquotation @{keyword}; changeset | files
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header; changeset | files
Thu, 15 Mar 2012 17:45:54 +0100 wenzelm more explicit header_edits before main text_edits; changeset | files
Thu, 15 Mar 2012 17:40:26 +0100 wenzelm declare keywords as side-effect of header edit; changeset | files
Thu, 15 Mar 2012 14:39:42 +0100 wenzelm more recent recent_syntax, e.g. relevant for document rendering during startup; changeset | files
Thu, 15 Mar 2012 14:22:54 +0100 wenzelm clarified syntax of prospective keywords; changeset | files
Thu, 15 Mar 2012 14:13:49 +0100 wenzelm basic support for outer syntax keywords in theory header; changeset | files
Thu, 15 Mar 2012 11:37:56 +0100 wenzelm maintain Version.syntax within document state; changeset | files
Thu, 15 Mar 2012 10:16:21 +0100 wenzelm explicit Outer_Syntax.Decl; changeset | files
Thu, 15 Mar 2012 09:55:42 +0100 wenzelm allow multiple 'keywords' as in 'fixes'; changeset | files
Thu, 15 Mar 2012 00:10:45 +0100 wenzelm some support for outer syntax keyword declarations within theory header; changeset | files
Wed, 14 Mar 2012 22:34:18 +0100 wenzelm merged changeset | files
Wed, 14 Mar 2012 17:19:30 +0000 paulson merged changeset | files
Wed, 14 Mar 2012 17:19:08 +0000 paulson structured case and induct rules changeset | files
Wed, 14 Mar 2012 17:40:00 +0100 haftmann rudimentary documentation test changeset | files
Wed, 14 Mar 2012 15:54:54 +0100 haftmann doc-src build option (for emerging mira configuration) changeset | files
Wed, 14 Mar 2012 15:54:27 +0100 haftmann corrected fragile proof; tuned semicolons changeset | files
Wed, 14 Mar 2012 15:24:51 +0100 haftmann rudimentary distribution build configuration changeset | files
Wed, 14 Mar 2012 15:24:07 +0100 haftmann support for non-HTTP repository locations (important for mira); quasi-hardwired repository name changeset | files
Wed, 14 Mar 2012 14:53:48 +0100 haftmann corrected slip changeset | files
Wed, 14 Mar 2012 12:39:26 +0000 paulson merged changeset | files
Wed, 14 Mar 2012 12:39:04 +0000 paulson rationalising the induction rule trans_induct3 changeset | files
Wed, 14 Mar 2012 12:20:42 +0100 haftmann allow modification of REPOS_NAME and REPOS from outside changeset | files
Wed, 14 Mar 2012 20:34:20 +0100 wenzelm locale expressions without source positions; changeset | files
Wed, 14 Mar 2012 19:27:15 +0100 wenzelm tuned; changeset | files
Wed, 14 Mar 2012 18:09:05 +0100 wenzelm tuned messages; changeset | files
Wed, 14 Mar 2012 17:52:38 +0100 wenzelm source positions for locale and class expressions; changeset | files
Wed, 14 Mar 2012 15:59:39 +0100 wenzelm some proof indentation; changeset | files
Wed, 14 Mar 2012 15:37:51 +0100 wenzelm more explicit indication of swing thread context; changeset | files
Wed, 14 Mar 2012 15:23:50 +0100 wenzelm more indentation; changeset | files
Wed, 14 Mar 2012 15:09:33 +0100 wenzelm prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks; changeset | files
Wed, 14 Mar 2012 14:49:43 +0100 wenzelm eliminated obsolete sanitize_name; changeset | files
Wed, 14 Mar 2012 11:45:16 +0100 wenzelm Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it; changeset | files
Wed, 14 Mar 2012 11:10:10 +0100 wenzelm more parallel inductive_cases; changeset | files
Wed, 14 Mar 2012 00:34:56 +0100 wenzelm misc tuning; changeset | files
Tue, 13 Mar 2012 23:45:34 +0100 wenzelm updated to jedit_build-20120313 with jedit-4.5.0; changeset | files
Tue, 13 Mar 2012 23:33:35 +0100 wenzelm tuned context specifications and proofs; changeset | files
Tue, 13 Mar 2012 22:49:02 +0100 wenzelm tuned proofs; changeset | files
Tue, 13 Mar 2012 21:17:37 +0100 wenzelm clarified command state -- markup within proper_range, excluding trailing whitespace; changeset | files
Tue, 13 Mar 2012 20:04:24 +0100 wenzelm more explicit indication of def names; changeset | files
Tue, 13 Mar 2012 17:17:52 +0000 paulson merged changeset | files
Tue, 13 Mar 2012 17:11:49 +0000 paulson Structured proofs concerning the square of an infinite cardinal changeset | files
Tue, 13 Mar 2012 17:04:00 +0100 wenzelm suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact"; changeset | files
Tue, 13 Mar 2012 16:56:56 +0100 wenzelm prefer abs_def over def_raw; changeset | files
Tue, 13 Mar 2012 16:40:06 +0100 wenzelm prefer abs_def over def_raw; changeset | files
Tue, 13 Mar 2012 16:22:18 +0100 wenzelm improved attribute "abs_def" to handle object-equality as well; changeset | files
Tue, 13 Mar 2012 14:44:27 +0100 wenzelm merged changeset | files
Tue, 13 Mar 2012 12:04:07 +0000 paulson More structured proofs about cardinal arithmetic changeset | files
Tue, 13 Mar 2012 14:44:16 +0100 wenzelm tuned proofs; changeset | files
Tue, 13 Mar 2012 14:17:42 +0100 wenzelm refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement; changeset | files
Tue, 13 Mar 2012 13:31:26 +0100 wenzelm tuned proofs -- eliminated pointless chaining of facts after 'interpret'; changeset | files
Tue, 13 Mar 2012 12:51:52 +0100 wenzelm proper printing of empty binding (again, cf. 93f6f24010c2); changeset | files
Tue, 13 Mar 2012 11:23:39 +0100 wenzelm tuned; changeset | files
Tue, 13 Mar 2012 11:22:39 +0100 wenzelm tuned strip_alls; changeset | files
Tue, 13 Mar 2012 11:21:26 +0100 wenzelm allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator; changeset | files
Mon, 12 Mar 2012 23:33:50 +0100 wenzelm some grouping of Par_List operations, to adjust granularity; changeset | files
Mon, 12 Mar 2012 23:16:54 +0100 wenzelm Par_List.map is already smart; changeset | files
Mon, 12 Mar 2012 23:16:02 +0100 wenzelm some support for grouped list operations; changeset | files
Mon, 12 Mar 2012 22:22:47 +0100 wenzelm merged; changeset | files
Mon, 12 Mar 2012 22:11:10 +0100 noschinl merged changeset | files
Mon, 12 Mar 2012 21:34:45 +0100 noschinl NEWS changeset | files
Mon, 12 Mar 2012 21:34:43 +0100 noschinl use eventually_elim method changeset | files
Mon, 12 Mar 2012 21:28:10 +0100 noschinl add eventually_elim method changeset | files
Mon, 12 Mar 2012 21:42:40 +0100 noschinl merged changeset | files
Mon, 12 Mar 2012 21:41:11 +0100 noschinl tuned proofs changeset | files
Mon, 12 Mar 2012 15:12:22 +0100 noschinl tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set changeset | files
Mon, 12 Mar 2012 15:11:24 +0100 noschinl tuned simpset changeset | files
Mon, 12 Mar 2012 21:31:22 +0100 wenzelm activate_notes in parallel -- to speedup main operation of locale interpretation; changeset | files
Mon, 12 Mar 2012 20:44:10 +0100 wenzelm refined activate_notes: simultaneous transformation before activation; changeset | files
Mon, 12 Mar 2012 19:09:38 +0100 wenzelm tuned headers; changeset | files
Mon, 12 Mar 2012 16:57:29 +0000 paulson merged changeset | files
Mon, 12 Mar 2012 16:14:25 +0000 paulson Structured proofs in ZF changeset | files
Mon, 12 Mar 2012 17:27:52 +0100 wenzelm refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state); changeset | files
Mon, 12 Mar 2012 16:04:00 +0100 wenzelm updated polyml/build option to prefer included libffi; changeset | files
Mon, 12 Mar 2012 15:31:30 +0100 wenzelm tuned signature; changeset | files
Mon, 12 Mar 2012 13:53:26 +0100 wenzelm clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports; changeset | files
Sun, 11 Mar 2012 22:06:13 +0100 wenzelm merged changeset | files
Sun, 11 Mar 2012 20:18:38 +0100 bulwahn renewing Executable_Relation changeset | files
Sun, 11 Mar 2012 22:06:12 +0100 wenzelm tuned; changeset | files
Sun, 11 Mar 2012 14:09:01 +0100 wenzelm more direct Name_Space.defined_entry; changeset | files
Sun, 11 Mar 2012 13:54:08 +0100 wenzelm eliminated old-fashioned 'constrains' element; changeset | files
Sun, 11 Mar 2012 13:39:16 +0100 wenzelm modernized locale expression, with some fluctuation of arguments; changeset | files
Sat, 10 Mar 2012 23:45:47 +0100 wenzelm simplified span class in conformance to Scala version; changeset | files
Sat, 10 Mar 2012 23:28:42 +0100 wenzelm discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name"); changeset | files
Sat, 10 Mar 2012 23:00:32 +0100 wenzelm merged changeset | files
Sat, 10 Mar 2012 16:39:55 +0100 bulwahn adding tags to quickcheck's result changeset | files
Sat, 10 Mar 2012 23:00:07 +0100 wenzelm clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval; changeset | files
Sat, 10 Mar 2012 22:02:45 +0100 wenzelm eliminated dead code; changeset | files
Sat, 10 Mar 2012 21:25:59 +0100 wenzelm clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway; changeset | files
Sat, 10 Mar 2012 20:58:40 +0100 wenzelm misc tuning and simplification; changeset | files
Sat, 10 Mar 2012 20:02:15 +0100 wenzelm tuned; changeset | files
Sat, 10 Mar 2012 19:49:32 +0100 wenzelm clarified Pattern.matchess; changeset | files
Sat, 10 Mar 2012 17:07:10 +0100 wenzelm tuned; changeset | files
Sat, 10 Mar 2012 16:49:34 +0100 wenzelm more precise alignment of begin/end, proof/qed; changeset | files
Fri, 09 Mar 2012 22:05:15 +0100 wenzelm merged changeset | files
Fri, 09 Mar 2012 21:50:27 +0100 haftmann beautified changeset | files
Fri, 09 Mar 2012 21:17:21 +0100 haftmann more precise checking for wellformedness of mapper, before and after morphism application changeset | files
Fri, 09 Mar 2012 20:50:28 +0100 haftmann reject mapper terms with type variables not contained in the term's type changeset | files
Fri, 09 Mar 2012 20:17:16 +0100 haftmann always bracket case expressions in Scala changeset | files
Fri, 09 Mar 2012 20:04:19 +0100 wenzelm tuned signature; changeset | files
Fri, 09 Mar 2012 17:24:42 +0000 paulson merges changeset | files
Fri, 09 Mar 2012 17:24:00 +0000 paulson More calculation-based cardinality proofs changeset | files
Fri, 09 Mar 2012 15:39:06 +0000 sultana split make_tptp_parser into two scripts, for parser and lib respectively; changeset | files
Fri, 09 Mar 2012 15:39:00 +0000 sultana added ml-yacc library sources; changeset | files
Fri, 09 Mar 2012 15:38:55 +0000 sultana added tptp parser; changeset | files
Thu, 08 Mar 2012 22:04:40 +0100 wenzelm merged changeset | files
Thu, 08 Mar 2012 16:49:24 +0000 paulson Structured and calculation-based proofs (with new trans rules!) changeset | files
Thu, 08 Mar 2012 16:43:29 +0000 paulson Structured and calculation-based proofs (with new trans rules!) changeset | files
Thu, 08 Mar 2012 21:40:15 +0100 wenzelm tuned comment; changeset | files
Thu, 08 Mar 2012 21:36:36 +0100 wenzelm simplified -- plain map_index is sufficient (pointed out by Enrico Tassi); changeset | files
Thu, 08 Mar 2012 21:35:54 +0100 wenzelm tuned; changeset | files
Thu, 08 Mar 2012 19:56:57 +0100 wenzelm clarified XML signature (again) -- coincide with basic Markup without explicit dependency; changeset | files
Thu, 08 Mar 2012 17:47:51 +0100 wenzelm more precise warning/error positions; changeset | files
Wed, 07 Mar 2012 23:21:00 +0100 wenzelm merged changeset | files
Wed, 07 Mar 2012 21:38:29 +0100 haftmann less rigorous but more realistic migration recommendation; note on code generation of sets changeset | files
Wed, 07 Mar 2012 21:34:36 +0100 haftmann tuned syntax; more candidates changeset | files
Wed, 07 Mar 2012 23:21:24 +0100 wenzelm tuned message (cf. ML version); changeset | files
Wed, 07 Mar 2012 20:49:18 +0100 wenzelm eliminated dead code; changeset | files
Wed, 07 Mar 2012 19:38:36 +0100 wenzelm tuned signature; changeset | files
Wed, 07 Mar 2012 19:32:52 +0100 wenzelm simplified signature (NB: interpretation of properties is mainly done via XML.Encode/Decode); changeset | files
Wed, 07 Mar 2012 16:13:49 +0100 berghofe to_pred/set attributes now properly handle variables of type "... => T set" changeset | files
Wed, 07 Mar 2012 14:30:35 +0100 wenzelm some recovery of IsaMakefile targets from f3c10e908f65; changeset | files
Wed, 07 Mar 2012 13:00:30 +0000 sultana added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults; changeset | files
Wed, 07 Mar 2012 13:00:30 +0000 sultana added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action; changeset | files
Wed, 07 Mar 2012 13:00:30 +0000 sultana added Mirabelle action info in its log file; tuned; changeset | files
Tue, 06 Mar 2012 17:01:37 +0000 paulson More mathematical symbols for ZF examples changeset | files
Tue, 06 Mar 2012 16:46:27 +0000 paulson mathematical symbols for Isabelle/ZF example theories changeset | files
Tue, 06 Mar 2012 16:06:52 +0000 paulson Using mathematical notation for <-> and cardinal arithmetic changeset | files
Tue, 06 Mar 2012 15:15:49 +0000 paulson mathematical symbols instead of ASCII changeset | files
Sun, 04 Mar 2012 23:20:43 +0100 blanchet addressed a quotient-type-related issue that arose with the port to "set" changeset | files
Sun, 04 Mar 2012 23:20:43 +0100 blanchet ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers) changeset | files
Sun, 04 Mar 2012 23:04:40 +0100 wenzelm updates for jedit-4.5.0 (still inactive); changeset | files
Sun, 04 Mar 2012 21:46:22 +0100 wenzelm more explicit patches; changeset | files
Sun, 04 Mar 2012 19:24:05 +0100 wenzelm tuned comment; changeset | files
Sun, 04 Mar 2012 19:16:09 +0100 wenzelm removed obsolete proper_command_at (cf. 03a2dc9e0624); changeset | files
Sun, 04 Mar 2012 19:03:28 +0100 wenzelm added Command.proper_range (still unused); changeset | files
Sun, 04 Mar 2012 18:15:45 +0100 wenzelm clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP"; changeset | files
Sun, 04 Mar 2012 16:02:14 +0100 wenzelm clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); changeset | files
Sun, 04 Mar 2012 11:03:10 +0100 haftmann tuned changeset | files
Sun, 04 Mar 2012 10:34:44 +0100 haftmann move test targets to test target changeset | files
Sun, 04 Mar 2012 10:33:47 +0100 haftmann dropped images for importer sessions changeset | files
Sun, 04 Mar 2012 00:29:19 +0100 haftmann dropped dead code changeset | files
Sun, 04 Mar 2012 00:27:07 +0100 haftmann more accurate dependencies changeset | files
Sun, 04 Mar 2012 00:26:23 +0100 haftmann tuned ML changeset | files
Sun, 04 Mar 2012 00:17:13 +0100 haftmann dropped silly code changeset | files
Sun, 04 Mar 2012 00:15:08 +0100 haftmann tuned changeset | files
Sun, 04 Mar 2012 00:04:37 +0100 haftmann dropped dead code changeset | files
Sun, 04 Mar 2012 00:03:21 +0100 haftmann actually add "the" Importer theory changeset | files
Sun, 04 Mar 2012 00:03:04 +0100 haftmann avoid internal hol4 name references in generic importer code changeset | files
Sat, 03 Mar 2012 23:54:44 +0100 haftmann generalized user-visible text changeset | files
Sat, 03 Mar 2012 23:49:54 +0100 haftmann generalized attribute name changeset | files
Sat, 03 Mar 2012 23:49:22 +0100 haftmann dropped dead theories changeset | files
Sat, 03 Mar 2012 23:43:21 +0100 haftmann one unified Importer theory changeset | files
Sat, 03 Mar 2012 23:42:56 +0100 haftmann added actual dependencies changeset | files
Sat, 03 Mar 2012 23:18:23 +0100 haftmann import all importer theories in compatibility layer changeset | files
Sat, 03 Mar 2012 22:53:24 +0100 wenzelm merged; changeset | files
Sat, 03 Mar 2012 22:46:34 +0100 haftmann dropped obsolete ROOT.ML changeset | files
Sat, 03 Mar 2012 22:38:53 +0100 haftmann plugged in pre-existing theories appropriately changeset | files
Sat, 03 Mar 2012 22:38:33 +0100 haftmann switch of target Import-HOL_Light-Imported: not operative at the moment changeset | files
Sat, 03 Mar 2012 22:38:11 +0100 haftmann turn on quick and dirty in batch mode changeset | files
Sat, 03 Mar 2012 22:37:56 +0100 haftmann tuned whitespace changeset | files
Sat, 03 Mar 2012 22:37:41 +0100 haftmann file system structure separating HOL4 and HOL Light concerns changeset | files
Sat, 03 Mar 2012 21:51:38 +0100 haftmann distribution of compatibility theories changeset | files
Sat, 03 Mar 2012 21:42:41 +0100 haftmann formal infrastructure for import sessions changeset | files
Sat, 03 Mar 2012 21:01:32 +0100 haftmann dropped dead code changeset | files
Sat, 03 Mar 2012 21:01:23 +0100 haftmann tuned whitespace changeset | files
Sat, 03 Mar 2012 21:00:31 +0100 haftmann spurious set/pred correction changeset | files
Sat, 03 Mar 2012 21:00:24 +0100 haftmann explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction changeset | files
Sat, 03 Mar 2012 21:00:04 +0100 haftmann explicit locations for import_theory and setup_theory, for better user interface conformance changeset | files
Sat, 03 Mar 2012 22:27:30 +0100 wenzelm discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I); changeset | files
Sat, 03 Mar 2012 22:17:52 +0100 wenzelm tuned; changeset | files
Sat, 03 Mar 2012 22:11:51 +0100 wenzelm tuned; changeset | files
Sat, 03 Mar 2012 21:52:15 +0100 wenzelm tuned; changeset | files
Sat, 03 Mar 2012 21:43:59 +0100 wenzelm canonical argument order for attribute application; changeset | files
Sat, 03 Mar 2012 18:18:39 +0100 wenzelm clarified terminology of raw protocol messages; changeset | files
Sat, 03 Mar 2012 17:46:50 +0100 wenzelm tuned; changeset | files
Sat, 03 Mar 2012 17:30:14 +0100 wenzelm tuned signature -- emphasize Isabelle_Process Input vs. Output; changeset | files
Sat, 03 Mar 2012 16:59:30 +0100 wenzelm explicit syslog_limit reduces danger of low-level message flooding; changeset | files
Sat, 03 Mar 2012 14:04:49 +0100 wenzelm retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); changeset | files
Sat, 03 Mar 2012 11:31:12 +0100 wenzelm clarified scope of exception handlers; changeset | files
Sat, 03 Mar 2012 11:09:17 +0100 wenzelm relevant timing as in ML; changeset | files
Fri, 02 Mar 2012 21:45:45 +0100 haftmann more fundamental pred-to-set conversions for range and domain by means of inductive_set changeset | files
Fri, 02 Mar 2012 22:57:57 +0100 wenzelm merged changeset | files
Fri, 02 Mar 2012 18:26:54 +0100 haftmann tuned whitespace changeset | files
Fri, 02 Mar 2012 15:18:05 +0100 haftmann tuned import changeset | files
Fri, 02 Mar 2012 15:17:54 +0100 haftmann dropped dead code changeset | files
Fri, 02 Mar 2012 22:34:42 +0100 wenzelm terminate after first exception -- avoid syslog flooding; changeset | files
Fri, 02 Mar 2012 21:22:42 +0100 wenzelm avoid buffer loading overrun; changeset | files
Fri, 02 Mar 2012 19:05:13 +0100 wenzelm merged changeset | files
Fri, 02 Mar 2012 09:35:39 +0100 bulwahn collecting all axioms in a locale context in quickcheck; changeset | files
Fri, 02 Mar 2012 09:35:35 +0100 bulwahn choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing changeset | files
Fri, 02 Mar 2012 09:35:33 +0100 bulwahn removing finiteness goals changeset | files
Fri, 02 Mar 2012 09:35:32 +0100 bulwahn adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets changeset | files
Thu, 01 Mar 2012 22:26:29 +0100 wenzelm Symbol.encode header edits; changeset | files
Thu, 01 Mar 2012 21:35:49 +0100 wenzelm merged changeset | files
Thu, 01 Mar 2012 19:35:02 +0100 haftmann tuned whitespace changeset | files
Thu, 01 Mar 2012 19:34:52 +0100 haftmann more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS) changeset | files
Thu, 01 Mar 2012 17:13:54 +0000 paulson Removal of obsolete ML bindings changeset | files
Thu, 01 Mar 2012 15:48:03 +0100 wenzelm more robust locking; changeset | files
Thu, 01 Mar 2012 15:42:44 +0100 wenzelm proper update_header; changeset | files
Thu, 01 Mar 2012 15:16:20 +0100 wenzelm refined node_header -- more direct buffer access (again); changeset | files
Thu, 01 Mar 2012 14:48:32 +0100 wenzelm merged changeset | files
Thu, 01 Mar 2012 11:28:56 +0100 blanchet improved handling of polymorphic quotient types, by avoiding comparing types that will generally differ in the polymorphic case changeset | files
Thu, 01 Mar 2012 11:28:56 +0100 blanchet fixed handling of "Rep_" function of quotient types -- side-effect of "set" constructor reintroduction changeset | files
Thu, 01 Mar 2012 11:28:56 +0100 blanchet more robust set element extractor changeset | files
Thu, 01 Mar 2012 10:12:58 +0100 boehmes fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates changeset | files
Thu, 01 Mar 2012 14:48:28 +0100 wenzelm tuned proofs; changeset | files
Thu, 01 Mar 2012 14:42:05 +0100 wenzelm more tolerant cygpath invocation, allow empty CLASSPATH; changeset | files
Thu, 01 Mar 2012 14:12:18 +0100 wenzelm explicitly revoke delay, to avoid spurious timer events after deactivation of related components; changeset | files
Thu, 01 Mar 2012 11:28:33 +0100 wenzelm clarified document nodes (full import graph) vs. node_status (non-preloaded theories); changeset | files
Wed, 29 Feb 2012 23:31:35 +0100 wenzelm more defensive node_header; changeset | files
Wed, 29 Feb 2012 23:09:06 +0100 wenzelm clarified module Thy_Load; changeset | files
Wed, 29 Feb 2012 17:43:41 +0100 boehmes SMT fails if the chosen SMT solver is not installed changeset | files
Tue, 28 Feb 2012 21:58:59 +0100 wenzelm merged changeset | files
Tue, 28 Feb 2012 15:54:51 +0100 blanchet speed up Sledgehammer's clasimpset lookup a bit changeset | files
Tue, 28 Feb 2012 15:54:51 +0100 blanchet use SPASS instead of E for Metis examples -- it's seems faster for these small problems changeset | files
Tue, 28 Feb 2012 15:54:51 +0100 blanchet spelling changeset | files
Tue, 28 Feb 2012 21:53:36 +0100 wenzelm avoid undeclared variables in let bindings; changeset | files
Tue, 28 Feb 2012 20:20:09 +0100 wenzelm tuned proofs; changeset | files
Tue, 28 Feb 2012 17:11:18 +0100 wenzelm more release tests; changeset | files
Tue, 28 Feb 2012 16:43:32 +0100 wenzelm display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69); changeset | files
Tue, 28 Feb 2012 14:24:37 +0100 Cezary Kaliszyk Finish localizing the quotient package. changeset | files
Tue, 28 Feb 2012 11:45:40 +0100 berghofe merged changeset | files
Tue, 28 Feb 2012 11:10:09 +0100 berghofe Added infrastructure for mapping SPARK field / constructor names changeset | files
Mon, 27 Feb 2012 10:32:39 +0100 berghofe Use long prefix rather than short package name to disambiguate constant names changeset | files
Mon, 27 Feb 2012 23:35:11 +0100 wenzelm more explicit development graph; changeset | files
Mon, 27 Feb 2012 23:30:38 +0100 wenzelm removed dead code (cf. a34d89ce6097); changeset | files
Mon, 27 Feb 2012 21:07:00 +0100 wenzelm tuned proofs; changeset | files
Mon, 27 Feb 2012 20:55:30 +0100 wenzelm tuned proofs; changeset | files
Mon, 27 Feb 2012 20:42:09 +0100 wenzelm removed introiff (cf. b09afce1e54f); changeset | files
Mon, 27 Feb 2012 20:33:18 +0100 wenzelm tuned; changeset | files
Mon, 27 Feb 2012 20:23:57 +0100 wenzelm removed broken/unused introiff (cf. d452117ba564); changeset | files
Mon, 27 Feb 2012 19:54:50 +0100 wenzelm discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling); changeset | files
Mon, 27 Feb 2012 19:53:34 +0100 wenzelm tuned; changeset | files
Mon, 27 Feb 2012 17:40:59 +0100 wenzelm tuned proofs; changeset | files
Mon, 27 Feb 2012 17:39:34 +0100 wenzelm prefer uniform Timing.message -- avoid assumption about sequential execution; changeset | files
Mon, 27 Feb 2012 17:13:25 +0100 wenzelm prefer final ADTs -- prevent ooddities; changeset | files
Mon, 27 Feb 2012 16:56:25 +0100 wenzelm more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile); changeset | files
Mon, 27 Feb 2012 16:53:13 +0100 wenzelm more standard settings -- refer to COMPONENT at most once; changeset | files
Mon, 27 Feb 2012 16:05:51 +0100 wenzelm clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well; changeset | files
Mon, 27 Feb 2012 15:48:02 +0100 wenzelm prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required; changeset | files
Mon, 27 Feb 2012 15:42:07 +0100 wenzelm eliminated odd comment from distant past; changeset | files
Mon, 27 Feb 2012 15:39:47 +0100 wenzelm updated cut_tac, without loose references to implementation manual; changeset | files
Mon, 27 Feb 2012 15:36:24 +0100 wenzelm updated generated file; changeset | files
Mon, 27 Feb 2012 15:00:19 +0100 wenzelm simplified cut_tac (cf. d549b5b0f344); changeset | files
Mon, 27 Feb 2012 14:07:59 +0100 huffman merged changeset | files
Mon, 27 Feb 2012 11:38:56 +0100 huffman avoid using constant Int.neg changeset | files
Mon, 27 Feb 2012 12:12:28 +0100 wenzelm reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository; changeset | files
Mon, 27 Feb 2012 11:53:08 +0100 nipkow merged changeset | files
Mon, 27 Feb 2012 10:27:21 +0100 nipkow added lemma changeset | files
Mon, 27 Feb 2012 09:01:49 +0100 nipkow converting "set [...]" to "{...}" in evaluation results changeset | files
Mon, 27 Feb 2012 10:56:36 +0100 bulwahn removing Find_Unused_Assms_Examples from session as it requires much time changeset | files
Sun, 26 Feb 2012 21:44:12 +0100 haftmann restored accidental omission changeset | files
Sun, 26 Feb 2012 21:43:57 +0100 haftmann dropped dead code changeset | files
Sun, 26 Feb 2012 21:26:28 +0100 haftmann tuned structure changeset | files
Sun, 26 Feb 2012 21:25:54 +0100 haftmann retain syntax here changeset | files
Sun, 26 Feb 2012 20:43:33 +0100 haftmann tuned structure; dropped already existing syntax declarations changeset | files
Sun, 26 Feb 2012 20:10:14 +0100 haftmann tuned syntax declarations; tuned structure changeset | files
Sun, 26 Feb 2012 20:08:12 +0100 wenzelm merged changeset | files
Sun, 26 Feb 2012 15:28:48 +0100 haftmann marked candidates for rule declarations changeset | files
Sun, 26 Feb 2012 20:05:14 +0100 wenzelm include warning messages in node status; changeset | files
Sun, 26 Feb 2012 19:36:35 +0100 wenzelm tuned signature (in accordance with ML); changeset | files
Sun, 26 Feb 2012 19:20:46 +0100 wenzelm more PIDE modules; changeset | files
Sun, 26 Feb 2012 18:26:26 +0100 wenzelm tuned proofs; changeset | files
Sun, 26 Feb 2012 18:25:28 +0100 wenzelm more abstract class Document.State; changeset | files
Sun, 26 Feb 2012 18:19:44 +0100 wenzelm more abstract class Document.State.Assignment; changeset | files
Sun, 26 Feb 2012 17:54:35 +0100 wenzelm tuned signature; changeset | files
Sun, 26 Feb 2012 17:44:09 +0100 wenzelm more abstract class Document.Version; changeset | files
Sun, 26 Feb 2012 17:15:33 +0100 wenzelm more abstract class Document.Node; changeset | files
Sun, 26 Feb 2012 16:58:28 +0100 wenzelm more abstract class Document.History; changeset | files
Sun, 26 Feb 2012 16:17:57 +0100 wenzelm more abstract class Document.Change; changeset | files
Sun, 26 Feb 2012 16:02:53 +0100 wenzelm tuned; changeset | files
Sun, 26 Feb 2012 15:18:48 +0100 wenzelm tuned signature; changeset | files
Sat, 25 Feb 2012 15:33:36 +0100 wenzelm merged changeset | files
Sat, 25 Feb 2012 09:07:53 +0100 bulwahn slightly changing the enumeration scheme changeset | files
Sat, 25 Feb 2012 09:07:51 +0100 bulwahn adding some more test invocations of find_unused_assms changeset | files
Sat, 25 Feb 2012 09:07:43 +0100 bulwahn adding an example where random beats exhaustive testing changeset | files
Sat, 25 Feb 2012 09:07:41 +0100 bulwahn removing unnecessary assumptions in RComplete; changeset | files
Sat, 25 Feb 2012 09:07:39 +0100 bulwahn removing unnecessary assumptions in RealDef; changeset | files
Sat, 25 Feb 2012 09:07:37 +0100 bulwahn one general list_all2_update_cong instead of two special ones changeset | files
Sat, 25 Feb 2012 13:17:38 +0100 wenzelm tuned comments; changeset | files
Sat, 25 Feb 2012 13:13:14 +0100 wenzelm standard Graph instances; changeset | files
Sat, 25 Feb 2012 13:00:32 +0100 wenzelm clarified signature -- avoid oddities of Iterable like Iterator.map; changeset | files
Sat, 25 Feb 2012 12:34:56 +0100 wenzelm discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map); changeset | files
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy changeset | files
Fri, 24 Feb 2012 22:46:16 +0100 haftmann explicit is better than implicit changeset | files
Fri, 24 Feb 2012 18:46:01 +0100 haftmann dropped dead code changeset | files
Fri, 24 Feb 2012 22:58:13 +0100 wenzelm prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty; changeset | files
Fri, 24 Feb 2012 22:15:19 +0100 wenzelm tuned imports; changeset | files
Fri, 24 Feb 2012 21:36:20 +0100 wenzelm tuned signature; changeset | files
Fri, 24 Feb 2012 20:37:52 +0100 wenzelm discontinued obsolete Graph.all_paths (last seen in 1524d69783d3 and AFP/80bbbdbfec62); changeset | files
Fri, 24 Feb 2012 19:47:11 +0100 wenzelm merged changeset | files
Fri, 24 Feb 2012 17:21:24 +0100 huffman remove ill-formed lemmas word_0_wi_Pls and word_m1_wi_Min changeset | files
Fri, 24 Feb 2012 16:59:20 +0100 huffman avoid using Int.succ_def in proofs changeset | files
Fri, 24 Feb 2012 16:55:29 +0100 huffman avoid using Int.succ or Int.pred in proofs changeset | files
Fri, 24 Feb 2012 16:53:59 +0100 huffman avoid using BIT_simps in proofs; changeset | files
Fri, 24 Feb 2012 16:46:43 +0100 huffman avoid using BIT_simps in proofs changeset | files
Fri, 24 Feb 2012 19:47:00 +0100 wenzelm updated stats according to src/HOL/IsaMakefile; changeset | files
Fri, 24 Feb 2012 19:45:10 +0100 wenzelm more precise clean target; changeset | files
Fri, 24 Feb 2012 18:14:06 +0100 wenzelm clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup; changeset | files
Fri, 24 Feb 2012 13:50:37 +0100 huffman avoid using Int.Pls_def in proofs changeset | files
Fri, 24 Feb 2012 13:37:23 +0100 huffman remove ill-formed lemmas word_pred_0_Min and word_m1_Min changeset | files
Fri, 24 Feb 2012 13:33:03 +0100 huffman remove ill-formed lemma of_bl_no; adapt proofs changeset | files
Fri, 24 Feb 2012 13:25:21 +0100 huffman adapt lemma mask_lem to respect int/bin distinction changeset | files
Fri, 24 Feb 2012 11:23:36 +0100 blanchet rephrase some slow "metis" calls changeset | files
Fri, 24 Feb 2012 11:23:35 +0100 blanchet added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization) changeset | files
Fri, 24 Feb 2012 11:23:34 +0100 blanchet general solution to the arity bug that occasionally plagues Sledgehammer -- short story, lots of things go kaputt when a polymorphic symbol's arity in the translation is higher than the arity of the fully polymorphic HOL constant changeset | files
Fri, 24 Feb 2012 11:23:34 +0100 blanchet renamed 'try_methods' to 'try0' changeset | files
Fri, 24 Feb 2012 11:23:33 +0100 blanchet doc fixes (thanks to Nik) changeset | files
Fri, 24 Feb 2012 11:23:32 +0100 blanchet fixed arity bug with "If" helpers for "If" that returns a function changeset | files
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch changeset | files
Fri, 24 Feb 2012 08:49:36 +0100 haftmann explicit remove of lattice notation changeset | files
Fri, 24 Feb 2012 07:30:24 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy changeset | files
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy changeset | files
Thu, 23 Feb 2012 21:16:54 +0100 haftmann dropped dead code changeset | files
Thu, 23 Feb 2012 22:07:12 +0100 wenzelm tuned isatest settings; changeset | files
Thu, 23 Feb 2012 21:39:11 +0100 wenzelm merged changeset | files
Thu, 23 Feb 2012 20:33:35 +0100 haftmann moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax changeset | files
Thu, 23 Feb 2012 20:15:59 +0100 haftmann tuned whitespace changeset | files
Thu, 23 Feb 2012 20:15:49 +0100 haftmann tuned proof changeset | files
Thu, 23 Feb 2012 21:15:11 +0100 wenzelm prefer actual syntax categories; changeset | files
Thu, 23 Feb 2012 20:40:20 +0100 wenzelm avoid trait Addable, which is deprecated in scala-2.9.x; changeset | files
Thu, 23 Feb 2012 20:24:05 +0100 wenzelm streamlined abstract datatype; changeset | files
Thu, 23 Feb 2012 20:23:19 +0100 wenzelm tuned; changeset | files
Thu, 23 Feb 2012 19:58:49 +0100 wenzelm streamlined abstract datatype; changeset | files
Thu, 23 Feb 2012 19:35:05 +0100 wenzelm tuned -- avoid copy of empty value; changeset | files
Thu, 23 Feb 2012 19:34:48 +0100 wenzelm tuned; changeset | files
Thu, 23 Feb 2012 18:38:30 +0100 wenzelm streamlined abstract datatype, eliminating odd representation class; changeset | files
Thu, 23 Feb 2012 18:14:58 +0100 wenzelm tuned; changeset | files
Thu, 23 Feb 2012 17:27:37 +0100 huffman merged changeset | files
Thu, 23 Feb 2012 16:09:16 +0100 huffman make more simp rules respect int/bin distinction changeset | files
Thu, 23 Feb 2012 15:37:42 +0100 huffman make bool list functions respect int/bin distinction changeset | files
Thu, 23 Feb 2012 16:18:19 +0100 wenzelm merged; changeset | files
Thu, 23 Feb 2012 16:02:07 +0100 wenzelm tuned; changeset | files
Thu, 23 Feb 2012 15:49:40 +0100 wenzelm clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations; changeset | files
Thu, 23 Feb 2012 15:15:59 +0100 wenzelm further graph operations from ML; changeset | files
Thu, 23 Feb 2012 14:46:38 +0100 wenzelm removed dead code; changeset | files
Thu, 23 Feb 2012 14:17:51 +0100 wenzelm directed graphs (in Scala); changeset | files
Thu, 23 Feb 2012 15:23:16 +0100 huffman make uses of bin_split respect int/bin distinction changeset | files
Thu, 23 Feb 2012 15:19:31 +0100 huffman remove lemma bin_cat_Pls, which doesn't respect int/bin distinction changeset | files
Thu, 23 Feb 2012 15:15:48 +0100 huffman make uses of constant bin_sc respect int/bin distinction changeset | files
Thu, 23 Feb 2012 15:04:51 +0100 huffman remove duplicate lemma bintrunc_Suc in favor of bintrunc.Suc changeset | files
Thu, 23 Feb 2012 14:43:01 +0100 huffman remove unused lemmas changeset | files
Thu, 23 Feb 2012 14:29:29 +0100 huffman simplify proofs changeset | files
Thu, 23 Feb 2012 13:16:18 +0100 huffman make uses of bin_sign respect int/bin distinction changeset | files
Thu, 23 Feb 2012 12:45:00 +0100 huffman removed unnecessary lemma zero_bintrunc changeset | files
Thu, 23 Feb 2012 12:24:34 +0100 huffman remove unnecessary lemmas changeset | files
Thu, 23 Feb 2012 12:08:59 +0100 huffman removed unnecessary constant bin_rl changeset | files
Thu, 23 Feb 2012 11:53:03 +0100 huffman remove duplication of lemmas bin_{rest,last}_BIT changeset | files
Thu, 23 Feb 2012 11:24:54 +0100 huffman remove lemmas Bit{0,1}_div2 changeset | files
Thu, 23 Feb 2012 11:20:42 +0100 huffman simplify proof changeset | files
Thu, 23 Feb 2012 08:59:55 +0100 huffman deal with FIXMEs for linarith examples changeset | files
Thu, 23 Feb 2012 08:17:22 +0100 haftmann CONTRIBUTORS changeset | files
Wed, 22 Feb 2012 19:59:06 +0100 huffman merged changeset | files
Wed, 22 Feb 2012 17:34:31 +0100 huffman tuned whitespace changeset | files
Wed, 22 Feb 2012 17:33:53 +0100 huffman tuned whitespace changeset | files
Wed, 22 Feb 2012 18:08:41 +0100 bulwahn adding documentation about find_unused_assms command and use_subtype option in the IsarRef changeset | files
Wed, 22 Feb 2012 18:08:27 +0100 bulwahn NEWS changeset | files
Wed, 22 Feb 2012 17:25:35 +0100 bulwahn adding some examples with find_unused_assms command changeset | files
Wed, 22 Feb 2012 17:22:53 +0100 bulwahn adding new command "find_unused_assms" changeset | files
Wed, 22 Feb 2012 12:30:01 +0100 bulwahn removing some unnecessary premises from Map theory changeset | files
Wed, 22 Feb 2012 09:35:01 +0100 bulwahn preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work) changeset | files
Wed, 22 Feb 2012 08:05:28 +0100 bulwahn generalizing inj_on_Int changeset | files
Wed, 22 Feb 2012 08:01:41 +0100 bulwahn moving Quickcheck's example to its own session changeset | files
Tue, 21 Feb 2012 23:25:36 +0100 wenzelm tuned proofs; changeset | files
Tue, 21 Feb 2012 23:24:49 +0100 wenzelm more robust visible_range: allow empty view; changeset | files
Tue, 21 Feb 2012 22:50:28 +0100 wenzelm misc tuning; changeset | files
Tue, 21 Feb 2012 21:15:57 +0100 wenzelm merged; changeset | files
Tue, 21 Feb 2012 20:43:58 +0100 wenzelm made SML/NJ happy; changeset | files
Tue, 21 Feb 2012 20:22:23 +0100 wenzelm tuned proofs; changeset | files
Tue, 21 Feb 2012 17:09:53 +0100 wenzelm merged changeset | files
Tue, 21 Feb 2012 17:09:17 +0100 wenzelm tuned proofs; changeset | files
Tue, 21 Feb 2012 17:08:32 +0100 wenzelm approximate Perspective.full within the bounds of the JVM; changeset | files
Tue, 21 Feb 2012 16:48:10 +0100 wenzelm misc tuning; changeset | files
Tue, 21 Feb 2012 16:42:57 +0100 wenzelm invoke later to reduce chance of causing deadlock; changeset | files
Tue, 21 Feb 2012 16:28:18 +0100 wenzelm misc tuning; changeset | files
Tue, 21 Feb 2012 16:04:58 +0100 wenzelm separate module for text status overview; changeset | files
Tue, 21 Feb 2012 15:36:23 +0100 wenzelm overview.delay_repaint: avoid wasting GUI cycles via update_delay; changeset | files
Tue, 21 Feb 2012 13:37:03 +0100 wenzelm tuned; changeset | files
Tue, 21 Feb 2012 13:19:16 +0100 berghofe merged changeset | files
Tue, 21 Feb 2012 12:10:47 +0100 berghofe merged changeset | files
Mon, 20 Feb 2012 16:09:58 +0100 berghofe Fixed bugs: changeset | files
Tue, 21 Feb 2012 13:15:25 +0100 bulwahn merged changeset | files
Tue, 21 Feb 2012 12:20:33 +0100 bulwahn subtype preprocessing in Quickcheck; changeset | files
Tue, 21 Feb 2012 11:25:48 +0100 bulwahn adding parsing of an optional predicate with quickcheck_generator command changeset | files
Tue, 21 Feb 2012 13:10:13 +0100 wenzelm updated generated files (cf. 8d51b375e926); changeset | files
Tue, 21 Feb 2012 12:45:00 +0100 wenzelm merged; changeset | files
Tue, 21 Feb 2012 11:08:05 +0100 huffman add missing lemmas to compute_div_mod changeset | files
Tue, 21 Feb 2012 11:04:38 +0100 huffman remove constant negateSnd in favor of 'apsnd uminus' (from Florian Haftmann) changeset | files
Tue, 21 Feb 2012 10:30:57 +0100 huffman avoid using constant Int.neg changeset | files
Tue, 21 Feb 2012 09:17:53 +0100 huffman renamed ex/Numeral.thy to ex/Numeral_Representation.thy changeset | files
Tue, 21 Feb 2012 08:15:42 +0100 haftmann reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems changeset | files
Mon, 20 Feb 2012 21:04:00 +0100 haftmann tuned whitespace changeset | files
Mon, 20 Feb 2012 08:01:08 +0100 haftmann tuned proof changeset | files
Sun, 19 Feb 2012 15:40:58 +0100 haftmann tuned proof changeset | files
Sun, 19 Feb 2012 15:30:35 +0100 haftmann distributed lattice properties of predicates to places of instantiation changeset | files
Mon, 20 Feb 2012 15:17:03 +0100 bulwahn removing some unnecessary premises from Divides changeset | files
Mon, 20 Feb 2012 14:23:46 +0100 huffman simplify projections on simultaneous computations of div and mod; tuned structure (from Florian Haftmann) changeset | files
Mon, 20 Feb 2012 22:35:32 +0100 wenzelm observe HEIGHT of overview ticks; changeset | files
Mon, 20 Feb 2012 20:24:01 +0100 wenzelm more careful painting of overview component: more precise and more efficient; changeset | files
Mon, 20 Feb 2012 15:36:48 +0100 wenzelm clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel; changeset | files
Mon, 20 Feb 2012 12:37:17 +0100 huffman use qualified constant names instead of suffixes (from Florian Haftmann) changeset | files
Sat, 18 Feb 2012 10:35:45 +0100 haftmann tuned proofs changeset | files
Sun, 12 Feb 2012 22:10:05 +0100 haftmann tuned changeset | files
Sat, 11 Feb 2012 00:07:28 +0100 haftmann brute-force adjustion changeset | files
Sat, 11 Feb 2012 00:06:48 +0100 haftmann tuned whitespace changeset | files
Sat, 11 Feb 2012 00:06:30 +0100 haftmann tuned changeset | files
Fri, 10 Feb 2012 23:56:09 +0100 haftmann tuned changeset | files
Fri, 10 Feb 2012 23:49:17 +0100 haftmann tuned code changeset | files
Fri, 10 Feb 2012 23:36:02 +0100 haftmann dropped whitespace changeset | files
Fri, 10 Feb 2012 23:30:17 +0100 haftmann dropped dead code changeset | files
Fri, 10 Feb 2012 23:23:41 +0100 haftmann dropped dead code changeset | files
Fri, 10 Feb 2012 23:16:24 +0100 haftmann dropped dead code changeset | files
Fri, 10 Feb 2012 23:14:23 +0100 haftmann dropped dead code changeset | files
Fri, 10 Feb 2012 23:12:57 +0100 haftmann dropped dead code changeset | files
Fri, 10 Feb 2012 23:06:21 +0100 haftmann dropped dead code changeset | files
Fri, 10 Feb 2012 22:58:04 +0100 haftmann corrected typo changeset | files
Fri, 10 Feb 2012 22:51:21 +0100 haftmann dropped dead code changeset | files
Sun, 12 Feb 2012 22:10:33 +0100 haftmann notepad is more appropriate here changeset | files
Sat, 18 Feb 2012 23:43:21 +0100 boehmes corrected treatment of applications of built-in functions to higher-order terms changeset | files
Sat, 18 Feb 2012 23:05:31 +0100 krauss NEWS changeset | files
Sat, 18 Feb 2012 22:31:24 +0100 krauss merged changeset | files
Sat, 18 Feb 2012 09:46:58 +0100 krauss added congruence rules for Option.{map|bind} changeset | files
Sat, 18 Feb 2012 20:53:39 +0100 haftmann updated generated documents changeset | files
Sat, 18 Feb 2012 20:50:11 +0100 haftmann avoid redefinition of @{theory} antiquotation changeset | files
Sat, 18 Feb 2012 20:13:38 +0100 haftmann update of generated documents changeset | files
Sat, 18 Feb 2012 20:12:37 +0100 haftmann tuned whitespace changeset | files
Sat, 18 Feb 2012 20:12:30 +0100 haftmann clarified changeset | files
Sat, 18 Feb 2012 20:12:16 +0100 haftmann corrected spelling changeset | files
Sat, 18 Feb 2012 20:11:58 +0100 haftmann clarified changeset | files
Sat, 18 Feb 2012 20:07:47 +0100 haftmann more precise semantics of "theory" antiquotation changeset | files
Sat, 18 Feb 2012 20:07:26 +0100 haftmann tuned import changeset | files
Sat, 18 Feb 2012 20:06:59 +0100 haftmann dropped references to obsolete theories changeset | files
Sat, 18 Feb 2012 20:06:43 +0100 haftmann adjusted to set type constructor changeset | files
Sat, 18 Feb 2012 20:06:14 +0100 haftmann tuned whitespace changeset | files
Sat, 18 Feb 2012 11:31:35 +0100 haftmann more explicit error on malformed abstract equation; dropped dead code; tuned signature changeset | files
Fri, 17 Feb 2012 15:42:26 +0100 wenzelm simplified configuration options for syntax ambiguity; changeset | files
Fri, 17 Feb 2012 11:24:39 +0100 wenzelm retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions); changeset | files
Thu, 16 Feb 2012 23:07:01 +0100 wenzelm more antiquotations; changeset | files
Thu, 16 Feb 2012 22:54:40 +0100 wenzelm more symbols; changeset | files
Thu, 16 Feb 2012 22:53:56 +0100 wenzelm tuned imports; changeset | files
Thu, 16 Feb 2012 22:53:24 +0100 wenzelm tuned proofs; changeset | files
Thu, 16 Feb 2012 22:18:28 +0100 wenzelm simplified configuration options for syntax ambiguity; changeset | files
Thu, 16 Feb 2012 17:09:15 +0100 wenzelm merged changeset | files
Thu, 16 Feb 2012 16:02:02 +0100 bulwahn removing unnecessary premise from diff_single_insert changeset | files
Thu, 16 Feb 2012 16:42:26 +0100 wenzelm explicit is better than implicit; changeset | files
Thu, 16 Feb 2012 14:14:58 +0100 wenzelm more uniform / portable representation of the idea of "copy_dir" (NB: cp -f dereferences symlinks on GNU/Linux, but does not on old-school Unixen including BSD/Mac OS X); changeset | files
Thu, 16 Feb 2012 09:51:34 +0100 bulwahn simplifying proof changeset | files
Thu, 16 Feb 2012 09:18:23 +0100 bulwahn removing unnecessary premises in theorems of List theory changeset | files
Thu, 16 Feb 2012 09:18:21 +0100 bulwahn tuning mutabelle script changeset | files
Thu, 16 Feb 2012 09:18:20 +0100 bulwahn adding documentation for abort_potential option in quickcheck changeset | files
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic; changeset | files
Wed, 15 Feb 2012 22:44:31 +0100 wenzelm discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component); changeset | files
Wed, 15 Feb 2012 21:38:28 +0100 wenzelm uniform Isar source formatting for this file; changeset | files
Wed, 15 Feb 2012 21:29:23 +0100 wenzelm clarified outer syntax "constdecl", which is only local to some rail diagrams; changeset | files
Wed, 15 Feb 2012 21:08:27 +0100 wenzelm discontinued obsolete "prems" fact; changeset | files
Wed, 15 Feb 2012 20:56:30 +0100 wenzelm eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba); changeset | files
Wed, 15 Feb 2012 20:47:32 +0100 wenzelm removed obsolete files; changeset | files
Wed, 15 Feb 2012 20:41:13 +0100 wenzelm more basic simplification, eliminated slightly odd tactic style from 1995 (cf. ea0668a1c0ba); changeset | files
Wed, 15 Feb 2012 20:28:19 +0100 wenzelm removed dead code; changeset | files
Wed, 15 Feb 2012 20:24:21 +0100 wenzelm updated listrel (cf. 80dccedd6c14); changeset | files
Wed, 15 Feb 2012 20:16:50 +0100 wenzelm removed redundant cut_inst_tac -- already covered in implementation manual; changeset | files
Wed, 15 Feb 2012 19:55:45 +0100 wenzelm updated rewrite_goals_rule, rewrite_rule; changeset | files
Wed, 15 Feb 2012 19:31:27 +0100 wenzelm NEWS; changeset | files
Wed, 15 Feb 2012 17:49:03 +0100 wenzelm updated refs; changeset | files
Wed, 15 Feb 2012 13:24:22 +0100 wenzelm renamed "xstr" to "str_token"; changeset | files
Tue, 14 Feb 2012 22:48:07 +0100 wenzelm merged changeset | files
Tue, 14 Feb 2012 20:13:07 +0100 blanchet don't report spurious LEO-II errors changeset | files
Tue, 14 Feb 2012 18:58:33 +0100 blanchet better error message changeset | files
Tue, 14 Feb 2012 17:59:10 +0100 bulwahn removing debug code in mutabelle changeset | files
Tue, 14 Feb 2012 17:58:51 +0100 bulwahn adding abort_potential functionality in quickcheck changeset | files
Tue, 14 Feb 2012 17:29:53 +0100 bulwahn adding abort_potential configuration in Quickcheck changeset | files
Tue, 14 Feb 2012 22:27:33 +0100 wenzelm clarified bires_inst_tac: retain internal exceptions; changeset | files
Tue, 14 Feb 2012 22:22:01 +0100 wenzelm tuned signature; changeset | files
Tue, 14 Feb 2012 21:59:10 +0100 wenzelm more conventional tactic setup -- avoid low-level Thm.dest_state and spurious warnings about it; changeset | files
Tue, 14 Feb 2012 21:45:32 +0100 wenzelm more conventional tactic setup; changeset | files
Tue, 14 Feb 2012 21:31:26 +0100 wenzelm eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac); changeset | files
Tue, 14 Feb 2012 21:19:39 +0100 wenzelm prefer high-level elim_format; changeset | files
Tue, 14 Feb 2012 20:57:05 +0100 wenzelm discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual; changeset | files
Tue, 14 Feb 2012 20:43:32 +0100 wenzelm method setup; changeset | files
Tue, 14 Feb 2012 20:09:35 +0100 wenzelm simplified use of tacticals; changeset | files
Tue, 14 Feb 2012 20:08:59 +0100 wenzelm comment; changeset | files
Tue, 14 Feb 2012 19:51:39 +0100 wenzelm tuned signature, according to actual usage of these operations; changeset | files
Tue, 14 Feb 2012 19:29:54 +0100 wenzelm tuned signature; changeset | files
Tue, 14 Feb 2012 19:18:57 +0100 wenzelm normalized aliases; changeset | files
Tue, 14 Feb 2012 17:54:08 +0100 wenzelm elininated unused INTLEAVE; changeset | files
Tue, 14 Feb 2012 17:51:29 +0100 wenzelm eliminated unused rewrite_goal_rule; changeset | files
Tue, 14 Feb 2012 17:49:47 +0100 wenzelm eliminated unused subgoals_tac; changeset | files
Tue, 14 Feb 2012 17:26:35 +0100 wenzelm eliminated obsolete aliases; changeset | files
Tue, 14 Feb 2012 17:11:33 +0100 wenzelm eliminated obsolete aliases; changeset | files
Tue, 14 Feb 2012 16:59:12 +0100 wenzelm tuned; changeset | files
Tue, 14 Feb 2012 12:40:55 +0100 wenzelm merged, resolving trivial conflicts; changeset | files
Tue, 14 Feb 2012 11:16:07 +0100 wenzelm merged; changeset | files
Sat, 11 Feb 2012 13:41:36 +0100 blanchet new SPASS options changeset | files
Sat, 11 Feb 2012 12:13:08 +0100 bulwahn making num_mutations a configuration that can be changed with the mutabelle bash command changeset | files
Sat, 11 Feb 2012 11:36:23 +0100 bulwahn making max_mutants an option that can be changed in the Mutabelle-script changeset | files
Sat, 11 Feb 2012 11:36:21 +0100 bulwahn increase timeout to 30 seconds; changing mutabelle script changeset | files
Fri, 10 Feb 2012 17:10:49 +0100 blanchet parse clauses generated from several formulas changeset | files
Fri, 10 Feb 2012 17:10:47 +0100 blanchet be more gentle when generating KBO weights changeset | files
Fri, 10 Feb 2012 16:33:58 +0100 blanchet update SPASS slices changeset | files
Fri, 10 Feb 2012 09:47:59 +0100 Cezary Kaliszyk more specification of the quotient package in IsarRef changeset | files
Fri, 10 Feb 2012 09:02:51 +0100 Cezary Kaliszyk specification of the quotient package changeset | files
Thu, 09 Feb 2012 16:00:04 +0100 blanchet tune KBO weight code changeset | files
Thu, 09 Feb 2012 14:42:18 +0100 blanchet minor DFG fix changeset | files
Thu, 09 Feb 2012 14:35:27 +0100 blanchet new SPASS slices changeset | files
Thu, 09 Feb 2012 14:04:17 +0100 blanchet improved KBO weights -- beware of explicit applications changeset | files
Thu, 09 Feb 2012 12:57:59 +0100 blanchet added possibility of generating KBO weights to DFG problems changeset | files
Thu, 09 Feb 2012 09:36:30 +0100 Cezary Kaliszyk Generalize the compositional preservation theorems changeset | files
Wed, 08 Feb 2012 01:49:33 +0100 blanchet use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules") changeset | files
Wed, 08 Feb 2012 00:55:06 +0100 blanchet removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly changeset | files
Wed, 08 Feb 2012 00:05:22 +0100 blanchet beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms changeset | files
Mon, 06 Feb 2012 23:01:02 +0100 blanchet fixed arity error changeset | files
Mon, 06 Feb 2012 23:01:02 +0100 blanchet tuning changeset | files
Mon, 06 Feb 2012 23:01:01 +0100 blanchet renamed type encoding changeset | files
Sun, 05 Feb 2012 17:43:15 +0100 bulwahn adding some forbidden constant names for mutabelle changeset | files
Sun, 05 Feb 2012 17:43:14 +0100 bulwahn mutabelle ignores theorems with internal constants changeset | files
Sun, 05 Feb 2012 17:09:21 +0100 nipkow tuned changeset | files
Sun, 05 Feb 2012 16:53:20 +0100 nipkow merged changeset | files
Sun, 05 Feb 2012 16:53:11 +0100 nipkow simplified code generation changeset | files
Sun, 05 Feb 2012 13:28:51 +0100 blanchet remove option that's on by default changeset | files
Sun, 05 Feb 2012 12:27:10 +0100 blanchet no need for a script/mega-hack with the new SPASS changeset | files
Sun, 05 Feb 2012 12:27:10 +0100 blanchet cleaned up new SPASS parsing changeset | files
Sun, 05 Feb 2012 12:27:10 +0100 blanchet tuning changeset | files
Sun, 05 Feb 2012 11:14:25 +0100 bulwahn merged changeset | files
Sun, 05 Feb 2012 10:43:52 +0100 bulwahn adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists changeset | files
Sun, 05 Feb 2012 10:42:57 +0100 bulwahn tuning to remove ML warnings changeset | files
Sun, 05 Feb 2012 10:50:34 +0100 blanchet removed double filtering of type args changeset | files
Sun, 05 Feb 2012 08:57:03 +0100 bulwahn adding a quickcheck example about functions and sets changeset | files
Sun, 05 Feb 2012 08:47:13 +0100 bulwahn removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since) changeset | files
Sun, 05 Feb 2012 08:36:41 +0100 bulwahn adding a remark about lemma which is too special and should be removed changeset | files
Sun, 05 Feb 2012 08:24:39 +0100 bulwahn another try to improve code generation of set equality (cf. da32cf32c0c7) changeset | files
Sun, 05 Feb 2012 08:24:38 +0100 bulwahn beautifying definitions of check_all and adding instance for finite_4 changeset | files
Sun, 05 Feb 2012 07:05:34 +0100 Cezary Kaliszyk Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients. changeset | files
Sat, 04 Feb 2012 17:01:25 +0100 blanchet added option to Mirabelle/Sledgehammer changeset | files
Sat, 04 Feb 2012 12:08:18 +0100 blanchet improved hashing w.r.t. Mirabelle, to help debugging changeset | files
Sat, 04 Feb 2012 12:08:18 +0100 blanchet tuned SPASS DFG output changeset | files
Sat, 04 Feb 2012 12:08:18 +0100 blanchet the new SPASS gives accurate fact information, so no need for old hack anymore changeset | files
Sat, 04 Feb 2012 12:08:18 +0100 blanchet fixed docs changeset | files
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made sure to filter type args also for "uncurried alias" equations changeset | files
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made option available to users (mostly for experiments) changeset | files
Sat, 04 Feb 2012 07:40:02 +0100 bulwahn using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a) changeset | files
Fri, 03 Feb 2012 18:00:55 +0100 blanchet optimization: slice caching in case two consecutive slices are nearly identical changeset | files
Fri, 03 Feb 2012 18:00:55 +0100 blanchet extended SPASS/DFG output with ranks changeset | files
Fri, 03 Feb 2012 18:00:55 +0100 blanchet try to pass fewer options to Metis changeset | files
Fri, 03 Feb 2012 15:51:10 +0100 Cezary Kaliszyk Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat changeset | files
Thu, 02 Feb 2012 19:41:58 +0100 blanchet improve SPASS scripts changeset | files
Thu, 02 Feb 2012 15:14:18 +0100 blanchet change 9ce354a77908 wasn't quite right -- here's an improvement changeset | files
Thu, 02 Feb 2012 12:51:03 +0100 blanchet better SPASS setup changeset | files
Thu, 02 Feb 2012 12:42:05 +0100 blanchet don't introduce new symbols in helpers -- makes problems unprovable changeset | files
Thu, 02 Feb 2012 12:42:05 +0100 blanchet only constants can be aliased changeset | files
Thu, 02 Feb 2012 12:42:05 +0100 blanchet include new SPASS by default if available changeset | files
Thu, 02 Feb 2012 10:16:10 +0100 bulwahn adding an example for finite and cofinite sets changeset | files
Thu, 02 Feb 2012 10:12:30 +0100 bulwahn adding a minimally refined equality on sets for code generation changeset | files
Thu, 02 Feb 2012 10:12:11 +0100 bulwahn adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type changeset | files
Wed, 01 Feb 2012 15:28:02 +0100 bulwahn improving code equations for multisets that violated the distinct AList abstraction changeset | files
Thu, 02 Feb 2012 01:55:17 +0100 blanchet tuning changeset | files
Thu, 02 Feb 2012 01:20:28 +0100 blanchet implemented partial application aliases (for SPASS mainly) changeset | files
Wed, 01 Feb 2012 17:16:55 +0100 blanchet really fixed syntax bug in DFG output (cf. ef62c2fafa9e) changeset | files
Wed, 01 Feb 2012 17:15:06 +0100 blanchet don't stumble on SPASS debug output changeset | files
Wed, 01 Feb 2012 14:53:46 +0100 blanchet tuning changeset | files
Wed, 01 Feb 2012 12:47:43 +0100 blanchet proper statuses for "fact_from_ref" changeset | files
Tue, 31 Jan 2012 19:38:36 +0100 nipkow tuned changeset | files
Tue, 31 Jan 2012 18:46:31 +0100 blanchet renamed Sledgehammer option changeset | files
Tue, 31 Jan 2012 17:09:08 +0100 blanchet third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9) changeset | files
Tue, 31 Jan 2012 16:11:15 +0100 blanchet improve SPASS setup changeset | files
Tue, 31 Jan 2012 15:39:45 +0100 bulwahn adding code equation for setsum changeset | files
Tue, 31 Jan 2012 15:13:18 +0100 blanchet avoid name clash, really changeset | files
Tue, 31 Jan 2012 15:10:03 +0100 blanchet fixed syntax bug in DFG output changeset | files
Tue, 31 Jan 2012 14:39:21 +0100 blanchet new SPASS setup changeset | files
Tue, 31 Jan 2012 12:43:48 +0100 blanchet distinguish between ":lr" and ":lt" (terminating) in DFG format changeset | files
Tue, 31 Jan 2012 10:29:05 +0100 blanchet nicer keyword class avoidance scheme changeset | files
Tue, 31 Jan 2012 10:29:04 +0100 blanchet new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0) changeset | files
Tue, 31 Jan 2012 09:06:27 +0100 bulwahn mutabelle must handle the case where quickcheck returns multiple results changeset | files
Tue, 31 Jan 2012 08:52:47 +0100 blanchet reverted e2b1a86d59fc -- broke Metis's lambda-lifting changeset | files
Tue, 31 Jan 2012 07:11:20 +0100 nipkow merged changeset | files
Tue, 31 Jan 2012 07:11:04 +0100 nipkow NEWS changeset | files
Mon, 30 Jan 2012 21:49:41 +0100 nipkow added "'a rel" changeset | files
Mon, 30 Jan 2012 22:56:09 +0100 blanchet fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers changeset | files
Mon, 30 Jan 2012 17:18:58 +0100 blanchet new SPASS setup changeset | files
Mon, 30 Jan 2012 17:15:59 +0100 blanchet example tuning changeset | files
Mon, 30 Jan 2012 17:15:59 +0100 blanchet implemented new lambda translations scheme changeset | files
Mon, 30 Jan 2012 17:15:59 +0100 blanchet avoid unsupported case in Metis changeset | files
Mon, 30 Jan 2012 17:15:59 +0100 blanchet docs and news changeset | files
Mon, 30 Jan 2012 17:15:59 +0100 blanchet rename lambda translation schemes changeset | files
Mon, 30 Jan 2012 17:15:59 +0100 blanchet example tuning changeset | files
Mon, 30 Jan 2012 13:55:28 +0100 bulwahn NEWS changeset | files
Mon, 30 Jan 2012 13:55:26 +0100 bulwahn renaming all lemmas with name rel_pow to relpow changeset | files
Mon, 30 Jan 2012 13:55:24 +0100 bulwahn adding code equations for max_extp and mlex changeset | files
Mon, 30 Jan 2012 13:55:23 +0100 bulwahn adding code generation for relpow by copying the ideas for code generation of funpow changeset | files
Mon, 30 Jan 2012 13:55:22 +0100 bulwahn adding code equation for rtranclp in Enum changeset | files
Mon, 30 Jan 2012 13:55:21 +0100 bulwahn adding code equation for max_ext changeset | files
Mon, 30 Jan 2012 13:55:20 +0100 bulwahn adding code equation for tranclp changeset | files
Mon, 30 Jan 2012 13:55:19 +0100 bulwahn adding code_unfold to make measure executable changeset | files
Sun, 29 Jan 2012 15:16:27 +0100 nipkow removed accidental dependance of abstract interpreter on gamma changeset | files
Sun, 29 Jan 2012 10:34:02 +0100 nipkow merged changeset | files
Sun, 29 Jan 2012 10:33:54 +0100 nipkow tuned changeset | files
Sat, 28 Jan 2012 12:05:26 +0100 bulwahn an executable version of accessible part (only for finite types yet) changeset | files
Sat, 28 Jan 2012 10:35:52 +0100 bulwahn adding yet another induction rule on natural numbers changeset | files
Sat, 28 Jan 2012 10:22:46 +0100 bulwahn moving declarations back to the section they seem to belong to (cf. afffe1f72143) changeset | files
Sat, 28 Jan 2012 06:13:03 +0100 bulwahn reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code changeset | files
Fri, 27 Jan 2012 19:08:48 +0100 bulwahn adding some more examples for quickcheck; replaced FIXME comments changeset | files
Fri, 27 Jan 2012 17:22:05 +0100 bulwahn new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well changeset | files
Fri, 27 Jan 2012 17:02:08 +0100 nipkow removed duplicate definitions that made locale inconsistent changeset | files
Fri, 27 Jan 2012 14:30:44 +0100 nipkow added parity analysis changeset | files
Fri, 27 Jan 2012 10:31:31 +0100 bulwahn corrected expectation; added an example for quickcheck changeset | files
Fri, 27 Jan 2012 10:31:30 +0100 bulwahn adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck changeset | files
Fri, 27 Jan 2012 10:19:55 +0100 blanchet made SML/NJ happy changeset | files
Thu, 26 Jan 2012 20:49:54 +0100 blanchet even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant changeset | files
Thu, 26 Jan 2012 20:49:54 +0100 blanchet separate orthogonal components changeset | files
Thu, 26 Jan 2012 20:49:54 +0100 blanchet generate left-to-right rewrite tag for combinator helpers for SPASS 3.8 changeset | files
Thu, 26 Jan 2012 20:49:54 +0100 blanchet better handling of individual type for DFG format (SPASS) changeset | files
Thu, 26 Jan 2012 12:04:05 +0100 bulwahn adding quickcheck example with THE changeset | files
Thu, 26 Jan 2012 12:03:35 +0100 bulwahn evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck. changeset | files
Thu, 26 Jan 2012 10:59:47 +0100 bulwahn using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 changeset | files
Thu, 26 Jan 2012 09:52:47 +0100 nipkow tuned changeset | files
Wed, 25 Jan 2012 16:07:48 +0100 bulwahn adding very basic code generation to Wellfounded theory changeset | files
Wed, 25 Jan 2012 16:07:41 +0100 bulwahn removing dead code from Mutabelle; tuned changeset | files
Wed, 25 Jan 2012 15:19:04 +0100 bulwahn generalizing check if size matters because it is different for random and exhaustive testing changeset | files
Wed, 25 Jan 2012 09:50:34 +0100 bulwahn merged changeset | files
Wed, 25 Jan 2012 09:32:23 +0100 bulwahn adding code equation for Collect on finite types changeset | files
Tue, 24 Jan 2012 16:00:51 +0100 berghofe Use lookup_size rather than Datatype.get_info in is_poly to avoid changeset | files
Tue, 24 Jan 2012 09:13:24 +0100 bulwahn adding some rules to quickcheck's preprocessing changeset | files
Tue, 24 Jan 2012 09:12:29 +0100 bulwahn some more constants on mutabelle's blacklist changeset | files
Mon, 23 Jan 2012 17:40:32 +0100 blanchet implemented "tptp_refute" tool changeset | files
Mon, 23 Jan 2012 17:40:32 +0100 blanchet added problem importer changeset | files
Mon, 23 Jan 2012 17:40:32 +0100 blanchet imported patch ATP_Problem_Import.thy changeset | files
Mon, 23 Jan 2012 17:40:32 +0100 blanchet imported patch atp_problem_import.ML changeset | files
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed theory exporter changeset | files
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file changeset | files
Mon, 23 Jan 2012 17:40:31 +0100 blanchet rebranded Nitrox, for more uniformity changeset | files
Mon, 23 Jan 2012 17:40:31 +0100 blanchet moved "nitrox" to TPTP changeset | files
Mon, 23 Jan 2012 17:29:19 +0100 huffman generalize type of List.listrel changeset | files
Mon, 23 Jan 2012 15:23:02 +0100 bulwahn support for Ex1 in quickcheck-narrowing changeset | files
Mon, 23 Jan 2012 15:22:33 +0100 bulwahn adding another internal constant to mutabelle's blacklust changeset | files
Mon, 23 Jan 2012 14:08:55 +0100 bulwahn adding some more forbidden constant names for the mutated conjecture generation changeset | files
Mon, 23 Jan 2012 14:07:36 +0100 bulwahn adding code generation for some list relations changeset | files
Mon, 23 Jan 2012 14:06:19 +0100 bulwahn adding fun_eq_iff to the preprocessing changeset | files
Mon, 23 Jan 2012 14:00:52 +0100 bulwahn random instance for sets changeset | files
Mon, 23 Jan 2012 11:59:00 +0100 bulwahn more configurations to mutabelle changeset | files
Fri, 20 Jan 2012 09:28:54 +0100 bulwahn catching code generation errors in quickcheck-narrowing changeset | files
Fri, 20 Jan 2012 09:28:53 +0100 bulwahn adding narrowing instance for sets changeset | files
Fri, 20 Jan 2012 09:28:52 +0100 bulwahn shortened definitions by adding some termify constants changeset | files
Fri, 20 Jan 2012 09:28:51 +0100 bulwahn tuned changeset | files
Fri, 20 Jan 2012 09:28:50 +0100 bulwahn adding check_all instance for sets; tuned changeset | files
Fri, 20 Jan 2012 08:24:51 +0100 nipkow tuned changeset | files
Fri, 20 Jan 2012 07:55:43 +0100 nipkow tuned changeset | files
Thu, 19 Jan 2012 21:37:12 +0100 blanchet minor edits in docs changeset | files
Thu, 19 Jan 2012 21:37:12 +0100 blanchet renamed "sound" option to "strict" changeset | files
Thu, 19 Jan 2012 21:37:12 +0100 blanchet updated Sledge docs some more changeset | files
Thu, 19 Jan 2012 21:37:12 +0100 blanchet more doc updates changeset | files
Thu, 19 Jan 2012 21:37:12 +0100 blanchet updated docs changeset | files
Thu, 19 Jan 2012 21:37:12 +0100 blanchet lower timeout for preplay, now that we have more preplay methods changeset | files
Thu, 19 Jan 2012 21:37:12 +0100 blanchet cleanly separate each Metis encoding changeset | files
Thu, 09 Feb 2012 19:34:23 +0100 wenzelm basic setup for equational reasoning; changeset | files
Tue, 07 Feb 2012 18:56:40 +0100 wenzelm tuned; changeset | files
Tue, 07 Feb 2012 18:51:22 +0100 wenzelm updated examples for syntax translations; changeset | files
Sun, 05 Feb 2012 21:00:38 +0100 wenzelm updated section on raw syntax; changeset | files
Sun, 05 Feb 2012 18:11:19 +0100 wenzelm updated section about syntax ambiguity; changeset | files
Sat, 04 Feb 2012 18:33:04 +0100 wenzelm updated/unified section on mixfix annotations; changeset | files
Sat, 04 Feb 2012 16:08:19 +0100 wenzelm tuned; changeset | files
Sat, 04 Feb 2012 15:56:49 +0100 wenzelm more on explicit notation; changeset | files
Sat, 04 Feb 2012 15:44:50 +0100 wenzelm more accurate Pure grammar; changeset | files
Sat, 04 Feb 2012 14:25:14 +0100 wenzelm more refs; changeset | files
Sat, 04 Feb 2012 14:20:39 +0100 wenzelm simplified mixfix (NB: infix is no longer required separately); changeset | files
Thu, 02 Feb 2012 21:21:41 +0100 wenzelm updated section on print modes; changeset | files
Thu, 02 Feb 2012 20:26:44 +0100 wenzelm misc tuning and reformatting; changeset | files
Thu, 02 Feb 2012 18:11:42 +0100 wenzelm clarified syntax section structure; changeset | files
Thu, 02 Feb 2012 17:52:16 +0100 wenzelm discontinued obscure history commands; changeset | files
Thu, 02 Feb 2012 16:38:15 +0100 wenzelm misc tuning and reformatting; changeset | files
Thu, 02 Feb 2012 16:07:25 +0100 wenzelm discontinued obscure history commands; changeset | files
Sun, 29 Jan 2012 22:12:25 +0100 wenzelm updated hint about asm_rl; changeset | files
Sun, 29 Jan 2012 22:00:10 +0100 wenzelm updated thin_tac; changeset | files
Sun, 29 Jan 2012 21:40:29 +0100 wenzelm updated distinct_subgoals_tac, flexflex_tac; changeset | files
Sun, 29 Jan 2012 21:26:09 +0100 wenzelm removed obscure material; changeset | files
Sun, 29 Jan 2012 21:04:39 +0100 wenzelm updated rotate_tac; changeset | files
Fri, 27 Jan 2012 21:56:29 +0100 wenzelm tuned; changeset | files
Fri, 27 Jan 2012 21:48:40 +0100 wenzelm updated citations; changeset | files
Fri, 27 Jan 2012 21:29:37 +0100 wenzelm updated subgoal_tac; changeset | files
Thu, 26 Jan 2012 22:21:33 +0100 wenzelm tuned sectioning; changeset | files
Thu, 26 Jan 2012 22:16:45 +0100 wenzelm updated "Control and search tacticals" (moved from ref to implementation); changeset | files
Thu, 26 Jan 2012 21:25:18 +0100 wenzelm obsolete -- covered in implementation manual; changeset | files
Thu, 26 Jan 2012 21:16:11 +0100 wenzelm moved HEADGOAL; changeset | files
Thu, 26 Jan 2012 15:29:11 +0100 wenzelm removed some obscure material; changeset | files
Thu, 26 Jan 2012 15:28:17 +0100 wenzelm added SELECT_GOAL; changeset | files
Thu, 26 Jan 2012 15:04:35 +0100 wenzelm tuned; changeset | files
Wed, 25 Jan 2012 22:01:15 +0100 wenzelm updated "subgoal quantifiers"; changeset | files
Wed, 25 Jan 2012 21:14:00 +0100 wenzelm tuned ML infixes; changeset | files
Wed, 25 Jan 2012 21:10:54 +0100 wenzelm document antiquotations for ML infix operators; changeset | files
Wed, 25 Jan 2012 20:26:05 +0100 wenzelm tuned; changeset | files
Wed, 25 Jan 2012 19:04:38 +0100 wenzelm updated repetition tacticals; changeset | files
Wed, 25 Jan 2012 18:18:59 +0100 wenzelm updated THEN, ORELSE, APPEND, and derivatives; changeset | files
Wed, 25 Jan 2012 16:16:20 +0100 wenzelm removed obscure/outdated material; changeset | files
Wed, 25 Jan 2012 15:39:08 +0100 wenzelm updated RSN, RL, RLN, MRS; changeset | files
Wed, 25 Jan 2012 14:13:59 +0100 wenzelm removed obscure/outdated material; changeset | files
Wed, 25 Jan 2012 13:31:56 +0100 wenzelm tuned; changeset | files
Wed, 25 Jan 2012 13:24:57 +0100 wenzelm more on Logic.all/mk_implies etc.; changeset | files
Thu, 19 Jan 2012 16:16:13 +0100 wenzelm reduce AFP test by many hours; changeset | files
Thu, 19 Jan 2012 09:51:42 +0100 nipkow added termination of narrowing changeset | files
Wed, 18 Jan 2012 22:06:31 +0100 wenzelm really need 64bit here; changeset | files
Wed, 18 Jan 2012 13:04:58 +0100 nipkow Added termination proof for widening changeset | files
Wed, 18 Jan 2012 22:09:29 +1100 kleing switch afp test to Darwin on macbroy2 changeset | files
Wed, 18 Jan 2012 10:05:23 +0100 nipkow merged changeset | files
Wed, 18 Jan 2012 10:05:14 +0100 nipkow introduced commands over a set of vars changeset | files
Wed, 18 Jan 2012 00:07:08 +0100 wenzelm basic support for PIDE Scala programming, independently of the main Isabelle repository; changeset | files
Tue, 17 Jan 2012 18:25:36 +0100 blanchet fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick changeset | files
Tue, 17 Jan 2012 18:25:36 +0100 blanchet updated message changeset | files
Tue, 17 Jan 2012 18:25:36 +0100 blanchet improve installation instructions changeset | files
Tue, 17 Jan 2012 18:25:36 +0100 blanchet allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script changeset | files
Tue, 17 Jan 2012 16:30:54 +0100 huffman factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero changeset | files
Tue, 17 Jan 2012 11:15:36 +0100 bulwahn refreshing NEWS changeset | files
Tue, 17 Jan 2012 10:45:42 +0100 bulwahn renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList) changeset | files
Tue, 17 Jan 2012 09:38:30 +0100 bulwahn renamed theory AList to DAList changeset | files
Mon, 16 Jan 2012 21:50:15 +0100 wenzelm position constraints for numerals enable PIDE markup; changeset | files
Mon, 16 Jan 2012 20:32:33 +0100 wenzelm more careful cumulation of tooltips -- ensure uniform range; changeset | files
Mon, 16 Jan 2012 13:19:44 +0100 wenzelm tuned; changeset | files
Mon, 16 Jan 2012 07:55:10 +0100 nipkow tuned changeset | files
Mon, 16 Jan 2012 07:46:58 +0100 nipkow missing dependency changeset | files
Sun, 15 Jan 2012 20:30:17 +0100 wenzelm tuned example; changeset | files
Sun, 15 Jan 2012 20:03:59 +0100 wenzelm merged changeset | files
Sun, 15 Jan 2012 19:55:31 +0100 wenzelm back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer; changeset | files
Sun, 15 Jan 2012 19:17:39 +0100 wenzelm recovered outdated_color (cf. 4beb2f41ed93); changeset | files
Sun, 15 Jan 2012 19:09:03 +0100 wenzelm more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages; changeset | files
Sun, 15 Jan 2012 18:55:27 +0100 wenzelm tuned proofs; changeset | files
Sun, 15 Jan 2012 17:27:46 +0100 nipkow tuned changeset | files
Sun, 15 Jan 2012 14:55:30 +0100 wenzelm tuned signature; changeset | files
Sun, 15 Jan 2012 14:22:54 +0100 wenzelm comments; changeset | files
Sun, 15 Jan 2012 14:17:42 +0100 wenzelm tuned proofs; changeset | files
Sun, 15 Jan 2012 14:00:07 +0100 wenzelm eliminated dead code, together with spurious warning about congruence rule for "Fun.comp"; changeset | files
Sun, 15 Jan 2012 13:55:01 +0100 wenzelm more explicit/robust treatment of common snapshot; changeset | files
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs; changeset | files
Sat, 14 Jan 2012 20:05:58 +0100 wenzelm renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all; changeset | files
Sat, 14 Jan 2012 19:06:05 +0100 wenzelm renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const; changeset | files
Sat, 14 Jan 2012 18:18:06 +0100 wenzelm tuned; changeset | files
Sat, 14 Jan 2012 17:45:04 +0100 wenzelm discontinued old-style Term.list_all_free in favour of plain Logic.all; changeset | files
Sat, 14 Jan 2012 16:58:29 +0100 wenzelm tuned; changeset | files
Sat, 14 Jan 2012 16:25:54 +0100 wenzelm discontinued default rendering for Oheimb's double-space; changeset | files
Sat, 14 Jan 2012 16:14:22 +0100 wenzelm tuned white space; changeset | files
Sat, 14 Jan 2012 16:12:09 +0100 wenzelm tuned comment; changeset | files
Sat, 14 Jan 2012 15:44:44 +0100 wenzelm paranoia null check -- prevent spurious crash of jedit token markup; changeset | files
Sat, 14 Jan 2012 15:30:54 +0100 wenzelm tuned comments; changeset | files
Sat, 14 Jan 2012 15:20:29 +0100 wenzelm tuned signature; changeset | files
Sat, 14 Jan 2012 14:34:42 +0100 wenzelm clarified partial restrict operation; changeset | files
Sat, 14 Jan 2012 13:22:39 +0100 wenzelm tuned proofs; changeset | files
Sat, 14 Jan 2012 13:11:32 +0100 wenzelm ignore empty gfx_range; changeset | files
Sat, 14 Jan 2012 12:36:43 +0100 wenzelm tuned signature; changeset | files
Fri, 13 Jan 2012 12:31:22 +0100 nipkow tuned changeset | files
Fri, 13 Jan 2012 11:55:06 +0100 wenzelm handle specific exception, not arbitrary ones (including Interrupt); changeset | files
Fri, 13 Jan 2012 11:50:28 +0100 wenzelm eliminated dead code; changeset | files
Thu, 12 Jan 2012 23:29:03 +0100 wenzelm more modest settings for lxbroy10 -- might actually perform better; changeset | files
Thu, 12 Jan 2012 22:05:54 +0100 wenzelm tuned; changeset | files
Thu, 12 Jan 2012 21:50:00 +0100 wenzelm improved select_markup: include filtering of defined results; changeset | files
Thu, 12 Jan 2012 21:21:22 +0100 wenzelm tuned text_color: cumulate with explicit default color; changeset | files
Thu, 12 Jan 2012 20:58:17 +0100 wenzelm added cat_lines convenience; changeset | files
Thu, 12 Jan 2012 20:57:37 +0100 wenzelm tuned; changeset | files
Thu, 12 Jan 2012 20:51:28 +0100 wenzelm clarified mkString: no extra line-breaks for XML.Body; changeset | files
Thu, 12 Jan 2012 10:19:33 +0100 bulwahn adding exhaustive instances for type constructor set changeset | files
Thu, 12 Jan 2012 00:14:20 +0100 berghofe Updated generated file changeset | files
Thu, 12 Jan 2012 00:13:37 +0100 berghofe Added inf_Int_eq to pred_set_conv database as well changeset | files
Wed, 11 Jan 2012 21:04:22 +0100 wenzelm more conventional eval_tac vs. method_setup "eval"; changeset | files
Wed, 11 Jan 2012 18:02:59 +0100 wenzelm updated generated file -- change of printed case syntax probably due to f805747f8571; changeset | files
Wed, 11 Jan 2012 17:30:34 +0100 wenzelm actually try to preserve names given by user (cf. 463b594e186a); changeset | files
Wed, 11 Jan 2012 16:47:30 +0100 wenzelm updated example -- List.foldl is no longer defined via primrec; changeset | files
Wed, 11 Jan 2012 16:25:34 +0100 wenzelm more qualified names; changeset | files
Wed, 11 Jan 2012 16:23:59 +0100 wenzelm refer to imp_cong from HOL, not Drule (!) -- cf. 4ed94d92ae19; changeset | files
Wed, 11 Jan 2012 15:12:57 +0100 wenzelm more robust ISABELLE_HOME_USER for repository versions -- some versions of Emacs interpret foo//bar as /bar even on the command-line (unlike regular POSIX semantics); changeset | files
Wed, 11 Jan 2012 00:05:31 +0100 berghofe merged changeset | files
Wed, 11 Jan 2012 00:01:54 +0100 berghofe Removed strange hack introduced in b27e93132603, since equivariance changeset | files
Tue, 10 Jan 2012 23:59:37 +0100 berghofe Replaced perm_set_eq by perm_set_def changeset | files
Tue, 10 Jan 2012 23:58:10 +0100 berghofe Corrected pt_set_inst, added missing cp_set_inst, deleted obsolete changeset | files
Tue, 10 Jan 2012 23:49:53 +0100 berghofe Reverted several lemmas involving sets to the state before the changeset | files
Tue, 10 Jan 2012 23:26:27 +0100 wenzelm clarified Isabelle_Rendering vs. physical painting; changeset | files
Tue, 10 Jan 2012 18:12:55 +0100 berghofe pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules changeset | files
Tue, 10 Jan 2012 18:12:03 +0100 berghofe pred_subset/equals_eq are now standard pred_set_conv rules changeset | files
Tue, 10 Jan 2012 18:09:09 +0100 berghofe Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules changeset | files
Tue, 10 Jan 2012 17:14:25 +0100 huffman merged changeset | files
Tue, 10 Jan 2012 15:43:16 +0100 huffman add simp rules for set_bit and msb applied to 0 and 1 changeset | files
Tue, 10 Jan 2012 14:48:42 +0100 huffman add simp rule test_bit_1 changeset | files
Tue, 10 Jan 2012 15:48:10 +0100 bulwahn proper hiding of facts and constants in AList_Impl and AList theory changeset | files
Tue, 10 Jan 2012 10:48:39 +0100 bulwahn NEWS changeset | files
Tue, 10 Jan 2012 10:18:08 +0100 bulwahn adding quickcheck examples with multisets changeset | files
Tue, 10 Jan 2012 10:17:09 +0100 bulwahn improving code generation for multisets; adding exhaustive quickcheck generators for multisets changeset | files
Tue, 10 Jan 2012 10:17:07 +0100 bulwahn adding theory association lists with invariant changeset | files
Mon, 09 Jan 2012 23:11:28 +0100 wenzelm command status color via regular markup; changeset | files
Mon, 09 Jan 2012 23:09:03 +0100 wenzelm proper cumulation of bulk arguments; changeset | files
Mon, 09 Jan 2012 23:08:33 +0100 wenzelm tuned; changeset | files
Mon, 09 Jan 2012 18:33:55 +0100 blanchet merge changeset | files
Mon, 09 Jan 2012 18:32:56 +0100 blanchet revert unintended "sledgehammer" call changeset | files
Mon, 09 Jan 2012 18:29:42 +0100 wenzelm prefer antiquotations; changeset | files
Mon, 09 Jan 2012 14:47:18 +0100 wenzelm misc tuning and reformatting; changeset | files
Mon, 09 Jan 2012 14:26:13 +0100 wenzelm updated generated file; changeset | files
Mon, 09 Jan 2012 13:48:14 +0100 nipkow Added termination to IMP Abs_Int changeset | files
Mon, 09 Jan 2012 11:41:38 +0100 nipkow added lemmas changeset | files
Sat, 07 Jan 2012 20:44:23 +0100 haftmann massaging of code setup for sets changeset | files
Sat, 07 Jan 2012 20:18:56 +0100 haftmann dropped theory More_Set changeset | files
Sat, 07 Jan 2012 20:18:56 +0100 haftmann use Inf/Sup_bool_def/apply as code equations changeset | files
Sat, 07 Jan 2012 21:19:53 +0100 nipkow tuned changeset | files
Sat, 07 Jan 2012 12:39:46 +0100 wenzelm accumulate status as regular markup for command range; changeset | files
Sat, 07 Jan 2012 11:45:53 +0100 haftmann corrected slip changeset | files
Sat, 07 Jan 2012 09:32:18 +0100 haftmann tuned changeset | files
Sat, 07 Jan 2012 09:32:01 +0100 haftmann restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets) changeset | files
Fri, 06 Jan 2012 22:16:25 +0100 haftmann moved lemmas about List.set and set operations to List theory changeset | files
Fri, 06 Jan 2012 22:16:01 +0100 haftmann moved lemmas about List.set and set operations to List theory changeset | files
Fri, 06 Jan 2012 21:48:45 +0100 haftmann incorporated various theorems from theory More_Set into corpus changeset | files
Fri, 06 Jan 2012 21:48:45 +0100 haftmann consolidated various theorem names relating to Finite_Set.fold and List.fold combinators changeset | files
Fri, 06 Jan 2012 20:48:52 +0100 wenzelm merged changeset | files
Fri, 06 Jan 2012 20:39:50 +0100 haftmann farewell to theory More_List changeset | files
Fri, 06 Jan 2012 11:15:02 +0100 haftmann dropped unused nth_map changeset | files
Fri, 06 Jan 2012 10:53:52 +0100 haftmann more explicit NEWS changeset | files
Fri, 06 Jan 2012 20:18:49 +0100 wenzelm refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x"; changeset | files
Fri, 06 Jan 2012 19:24:23 +0100 wenzelm tuned; changeset | files
Fri, 06 Jan 2012 17:44:42 +0100 wenzelm improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup; changeset | files
Fri, 06 Jan 2012 16:45:19 +0100 wenzelm tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable); changeset | files
Fri, 06 Jan 2012 16:42:15 +0100 wenzelm recovered case syntax for of_int, also with source positions (appears to be unused nonetheless); changeset | files
Fri, 06 Jan 2012 15:19:17 +0100 wenzelm more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables); changeset | files
Fri, 06 Jan 2012 11:27:49 +0100 wenzelm proper refs; changeset | files
Fri, 06 Jan 2012 10:19:49 +0100 haftmann incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r) changeset | files
Fri, 06 Jan 2012 10:19:49 +0100 haftmann incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes changeset | files
Fri, 06 Jan 2012 10:19:48 +0100 haftmann prefer listsum over foldl plus 0 changeset | files
Fri, 06 Jan 2012 10:19:48 +0100 haftmann prefer concat over foldl append [] changeset | files
Fri, 06 Jan 2012 10:19:47 +0100 haftmann tuned proofs changeset | files
Sun, 01 Jan 2012 15:44:15 +0100 haftmann interaction of set operations for execution and membership predicate changeset | files
Sun, 01 Jan 2012 11:28:45 +0100 haftmann cleanup of code declarations changeset | files
Thu, 05 Jan 2012 20:26:01 +0100 wenzelm discontinued Syntax.positions -- atomic parse trees are always annotated; changeset | files
Thu, 05 Jan 2012 18:18:39 +0100 wenzelm improved case syntax: more careful treatment of position constraints, which enables PIDE markup; changeset | files
Thu, 05 Jan 2012 15:31:49 +0100 wenzelm misc tuning; changeset | files
Thu, 05 Jan 2012 14:48:41 +0100 wenzelm prefer raw_message for protocol implementation; changeset | files
Thu, 05 Jan 2012 14:34:18 +0100 wenzelm prefer raw_message for protocol implementation; changeset | files
Thu, 05 Jan 2012 14:15:37 +0100 wenzelm prefer raw_message for protocol implementation; changeset | files
Thu, 05 Jan 2012 13:27:50 +0100 wenzelm tuned signature; changeset | files
Thu, 05 Jan 2012 13:24:29 +0100 wenzelm tuned signature -- emphasize special nature of protocol commands; changeset | files
Thu, 05 Jan 2012 10:59:18 +0100 wenzelm updated version information; changeset | files
Wed, 04 Jan 2012 15:41:18 +0100 wenzelm updated version information; changeset | files
Wed, 04 Jan 2012 13:58:06 +0100 nipkow generalised type changeset | files
Wed, 04 Jan 2012 12:09:53 +0100 blanchet improved "set" support by code inspection changeset | files
Wed, 04 Jan 2012 12:09:53 +0100 blanchet remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder changeset | files
Wed, 04 Jan 2012 12:09:53 +0100 blanchet tuning changeset | files
Wed, 04 Jan 2012 12:09:53 +0100 blanchet handle higher-order occurrences of sets gracefully in model display changeset | files
Wed, 04 Jan 2012 11:01:08 +0100 wenzelm prefer explicit version information; changeset | files
Wed, 04 Jan 2012 10:47:07 +0100 blanchet more Nitpick doc updates changeset | files
Wed, 04 Jan 2012 00:32:02 +0100 blanchet reenable Kodkodi in Mira now that Nitpick has been ported to 'a set constructor changeset | files
Wed, 04 Jan 2012 00:30:53 +0100 blanchet reenable Kodkodi in Isatest now that Nitpick has been ported to 'a set constructor changeset | files
Tue, 03 Jan 2012 23:41:59 +0100 blanchet fixed bisimilarity axiom -- avoid "insert" with wrong type changeset | files
Tue, 03 Jan 2012 23:09:27 +0100 blanchet tuning changeset | files
Tue, 03 Jan 2012 23:03:49 +0100 blanchet updated Nitpick docs after "set" reintroduction changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet no abuse of notation changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual) changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet more robust destruction of "set Collect" idiom changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet handle starred predicates correctly w.r.t. "set" changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet handle "Id" gracefully w.r.t. "set" changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet handle "set" correctly in Refute -- inspired by old code from Isabelle2007 changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet create consts with proper "set" types changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet tuned Refute changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet lower cardinality for faster testing changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet simplify mem Collect changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet tuning changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet ported Minipick to "set" changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet fixed set extensionality code changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet tuned import changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet construct correct "set" type for wf goal changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet fixed Nitpick's typedef handling w.r.t. "set" changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet fixed type annotations changeset | files
Tue, 03 Jan 2012 18:33:18 +0100 blanchet rationalized output (a bit) changeset | files
Tue, 03 Jan 2012 18:33:17 +0100 blanchet fixed a few more bugs in \Nitpick's new "set" support changeset | files
Tue, 03 Jan 2012 18:33:17 +0100 blanchet regenerate SMT example certificates, to reflect "set" type constructor changeset | files
Tue, 03 Jan 2012 18:33:17 +0100 blanchet port part of Nitpick to "set" type constructor changeset | files
Tue, 03 Jan 2012 18:33:17 +0100 blanchet reintroduced failing examples now that they work again, after reintroduction of "set" changeset | files
Tue, 03 Jan 2012 18:33:17 +0100 blanchet ported mono calculus to handle "set" type constructors changeset | files
Tue, 03 Jan 2012 18:33:17 +0100 blanchet fixed spurious catch-all patterns changeset | files
Tue, 03 Jan 2012 13:06:03 +0100 wenzelm more benchmarks; changeset | files
Mon, 02 Jan 2012 20:25:21 +0100 nipkow tuned changeset | files
Mon, 02 Jan 2012 15:15:46 +0100 blanchet ported "Sets" example to "set" type constructor changeset | files
Mon, 02 Jan 2012 15:08:40 +0100 blanchet ported a dozen of proofs to the "set" type constructor changeset | files
Mon, 02 Jan 2012 14:45:13 +0100 blanchet reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow changeset | files
Mon, 02 Jan 2012 14:36:49 +0100 blanchet update docs to reflect "Manual_Nits" changeset | files
Mon, 02 Jan 2012 14:32:20 +0100 blanchet removed special handling for set constants in relevance filter changeset | files
Mon, 02 Jan 2012 14:26:57 +0100 blanchet reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter changeset | files
Mon, 02 Jan 2012 14:12:20 +0100 blanchet killed unfold_set_const option that makes no sense now that set is a type constructor again changeset | files
Mon, 02 Jan 2012 11:54:21 +0100 nipkow tuned changeset | files
Mon, 02 Jan 2012 11:33:50 +0100 nipkow removed unnecessary lemmas changeset | files
Mon, 02 Jan 2012 10:51:28 +0100 nipkow tuned proofs changeset | files
Sun, 01 Jan 2012 18:12:11 +0100 nipkow tuned var names changeset | files
Sun, 01 Jan 2012 16:32:53 +0100 nipkow tuned argument order changeset | files
Sun, 01 Jan 2012 09:27:48 +0100 huffman merged changeset | files
Fri, 30 Dec 2011 16:08:35 +0100 huffman add simp rules for bitwise word operations with 1 changeset | files
Sat, 31 Dec 2011 17:53:50 +0100 nipkow tuned types changeset | files
Sat, 31 Dec 2011 10:15:53 +0100 krauss disabled failing sledgehammer unit test (collateral damage of 184d36538e51) changeset | files
Sat, 31 Dec 2011 00:19:32 +0100 krauss disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5) changeset | files
Fri, 30 Dec 2011 18:14:56 +0100 berghofe merged changeset | files
Fri, 30 Dec 2011 18:12:00 +0100 berghofe Made gen_dest_case more robust against eta contraction changeset | files
Fri, 30 Dec 2011 17:45:13 +0100 wenzelm merged changeset | files
Fri, 30 Dec 2011 11:11:57 +0100 huffman remove unnecessary intermediate lemmas changeset | files
Fri, 30 Dec 2011 17:40:30 +0100 wenzelm tuned; changeset | files
Fri, 30 Dec 2011 16:43:46 +0100 wenzelm eliminated old-fashioned Global_Theory.add_thms; changeset | files
Fri, 30 Dec 2011 15:43:07 +0100 wenzelm simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac; changeset | files
Fri, 30 Dec 2011 14:19:58 +0100 wenzelm simplified proof; changeset | files
Fri, 30 Dec 2011 13:52:07 +0100 wenzelm simplified proof; changeset | files
Fri, 30 Dec 2011 12:54:55 +0100 wenzelm simplified proof; changeset | files
Fri, 30 Dec 2011 12:12:16 +0100 wenzelm more parallelism; changeset | files
Fri, 30 Dec 2011 12:00:10 +0100 wenzelm tuned; changeset | files
Thu, 29 Dec 2011 20:32:59 +0100 wenzelm merged changeset | files
Thu, 29 Dec 2011 20:31:58 +0100 wenzelm tuned -- afford slightly larger simpset in simp_defs_tac; changeset | files
Thu, 29 Dec 2011 20:05:53 +0100 wenzelm tuned -- standard proofs by default; changeset | files
Thu, 29 Dec 2011 19:37:24 +0100 wenzelm do not fork skipped proofs; changeset | files
Thu, 29 Dec 2011 18:27:17 +0100 wenzelm clarified timeit_msg; changeset | files
Thu, 29 Dec 2011 16:58:19 +0100 wenzelm tuned; changeset | files
Thu, 29 Dec 2011 15:54:37 +0100 wenzelm comments; changeset | files
Thu, 29 Dec 2011 18:54:07 +0100 huffman remove constant 'ccpo.lub', re-use constant 'Sup' instead changeset | files
Thu, 29 Dec 2011 17:43:54 +0100 nipkow merged changeset | files
Thu, 29 Dec 2011 17:43:40 +0100 nipkow tuned changeset | files
Thu, 29 Dec 2011 15:14:44 +0100 haftmann conversions from sets to predicates and vice versa; extensionality on predicates changeset | files
Thu, 29 Dec 2011 15:14:44 +0100 haftmann added implementation of pred_of_set changeset | files
Thu, 29 Dec 2011 14:23:40 +0100 haftmann fundamental theorems on Set.bind changeset | files
Thu, 29 Dec 2011 14:44:44 +0100 wenzelm updated generated files; changeset | files
Thu, 29 Dec 2011 13:42:21 +0100 haftmann qualified Finite_Set.fold changeset | files
Thu, 29 Dec 2011 13:41:41 +0100 haftmann qualified Finite_Set.fold changeset | files
Thu, 29 Dec 2011 10:47:56 +0100 haftmann dropped redundant setup changeset | files
Thu, 29 Dec 2011 10:47:56 +0100 haftmann tuned declaration changeset | files
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post; tuned text changeset | files
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post; tuned names and spacing changeset | files
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post changeset | files
Thu, 29 Dec 2011 10:47:55 +0100 haftmann semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat; attribute code_abbrev superseedes code_unfold_post changeset | files
Thu, 29 Dec 2011 10:47:54 +0100 haftmann semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat changeset | files
Wed, 28 Dec 2011 22:08:44 +0100 wenzelm merged changeset | files
Wed, 28 Dec 2011 20:05:52 +0100 huffman merged changeset | files
Wed, 28 Dec 2011 20:05:28 +0100 huffman restate some lemmas to respect int/bin distinction changeset | files
Wed, 28 Dec 2011 19:15:28 +0100 huffman simplify some proofs changeset | files
Wed, 28 Dec 2011 18:50:35 +0100 huffman add lemma word_eq_iff changeset | files
Wed, 28 Dec 2011 18:33:03 +0100 huffman restate lemma word_1_no in terms of Numeral1 changeset | files
Wed, 28 Dec 2011 18:27:34 +0100 huffman remove recursion combinator bin_rec; changeset | files
Wed, 28 Dec 2011 16:24:28 +0100 huffman simplify definition of XOR for type int; changeset | files
Wed, 28 Dec 2011 16:10:49 +0100 huffman simplify definition of OR for type int; changeset | files
Wed, 28 Dec 2011 16:04:58 +0100 huffman simplify definition of NOT for type int changeset | files
Wed, 28 Dec 2011 13:20:46 +0100 huffman add several new tests, most of which don't work yet changeset | files
Wed, 28 Dec 2011 12:55:37 +0100 huffman fix typos changeset | files
Wed, 28 Dec 2011 12:52:23 +0100 huffman remove some duplicate lemmas changeset | files
Wed, 28 Dec 2011 10:48:39 +0100 huffman simplify proof changeset | files
Wed, 28 Dec 2011 10:30:43 +0100 huffman replace 'lemmas' with explicit 'lemma' changeset | files
Wed, 28 Dec 2011 07:58:17 +0100 huffman add section headings changeset | files
Tue, 27 Dec 2011 18:26:15 +0100 huffman remove duplicate lemma lists changeset | files
Wed, 28 Dec 2011 20:03:13 +0100 wenzelm reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008"; changeset | files
Wed, 28 Dec 2011 15:08:12 +0100 wenzelm disable kodkodi for now to prevent isatest failure of HOL-Nitpick_Examples due to 'a set constructor; changeset | files
Wed, 28 Dec 2011 14:38:14 +0100 wenzelm updated platform information; changeset | files
Wed, 28 Dec 2011 13:13:27 +0100 wenzelm discontinued broken macbroy5 and thus the obsolete ppc-darwin platform; changeset | files
Wed, 28 Dec 2011 13:08:18 +0100 wenzelm more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms; changeset | files
Wed, 28 Dec 2011 13:00:51 +0100 wenzelm print case syntax depending on "show_cases" configuration option; changeset | files
Tue, 27 Dec 2011 15:38:45 +0100 huffman merged changeset | files
Tue, 27 Dec 2011 15:37:33 +0100 huffman redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min changeset | files
Tue, 27 Dec 2011 13:16:22 +0100 huffman remove some uses of Int.succ and Int.pred changeset | files
Tue, 27 Dec 2011 12:49:03 +0100 huffman removed unused lemmas changeset | files
Tue, 27 Dec 2011 12:37:11 +0100 huffman remove redundant syntax declaration changeset | files
Tue, 27 Dec 2011 12:27:06 +0100 huffman use 'induct arbitrary' instead of 'rule_format' attribute changeset | files
Tue, 27 Dec 2011 12:05:03 +0100 huffman declare simp rules immediately, instead of using 'declare' commands changeset | files
Tue, 27 Dec 2011 11:38:55 +0100 huffman declare word_of_int_{0,1} [simp], for consistency with word_of_int_bin changeset | files
Tue, 27 Dec 2011 09:45:10 +0100 haftmann be explicit about Finite_Set.fold changeset | files
Tue, 27 Dec 2011 09:15:26 +0100 haftmann dropped fact whose names clash with corresponding facts on canonical fold changeset | files
Tue, 27 Dec 2011 09:15:26 +0100 haftmann prefer canonical fold on lists changeset | files
Tue, 27 Dec 2011 09:15:26 +0100 haftmann be explicit about Finite_Set.fold changeset | files
Mon, 26 Dec 2011 22:17:10 +0100 haftmann incorporated More_Set and More_List into the Main body -- to be consolidated later changeset | files
Mon, 26 Dec 2011 22:17:10 +0100 haftmann moved theorem requiring multisets from More_List to Multiset changeset | files
Mon, 26 Dec 2011 22:17:10 +0100 haftmann NEWS: unavoidable fact renames changeset | files
Mon, 26 Dec 2011 18:32:43 +0100 haftmann dropped disfruitful `constant signatures` changeset | files
Mon, 26 Dec 2011 18:32:43 +0100 haftmann moved various set operations to theory Set (resp. Product_Type) changeset | files
Mon, 26 Dec 2011 17:40:43 +0100 haftmann dropped Executable_Set wrapper theory changeset | files
Sun, 25 Dec 2011 08:42:33 +0100 haftmann updated certificate changeset | files
Sat, 24 Dec 2011 16:14:59 +0100 haftmann NEWS: `set` is now a proper type constructor changeset | files
Sat, 24 Dec 2011 16:14:58 +0100 haftmann dropped references to obsolete facts `mem_def` and `Collect_def` changeset | files
Sat, 24 Dec 2011 16:14:58 +0100 haftmann dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw` changeset | files
Sat, 24 Dec 2011 16:14:58 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set` changeset | files
Sat, 24 Dec 2011 16:14:58 +0100 haftmann treatment of type constructor `set` changeset | files
Sat, 24 Dec 2011 15:55:03 +0100 haftmann executable intervals changeset | files
Sat, 24 Dec 2011 15:54:58 +0100 haftmann `set` is now a proper type constructor changeset | files
Sat, 24 Dec 2011 15:53:12 +0100 haftmann tuned layout changeset | files
Sat, 24 Dec 2011 15:53:12 +0100 haftmann reduced to a compatibility layer changeset | files
Sat, 24 Dec 2011 15:53:11 +0100 haftmann added setup for executable code changeset | files
(0) -30000 -10000 -1920 +1920 +10000 +30000 tip
isabelle