Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
Wed, 14 Oct 2009 16:23:32 +0200 Cezary Kaliszyk Manually regularized list_induct2 file | diff | annotate
Wed, 14 Oct 2009 12:05:39 +0200 Cezary Kaliszyk Fixed bug in regularise types. Now we can regularise list.induct. file | diff | annotate
Wed, 14 Oct 2009 11:23:55 +0200 Cezary Kaliszyk Function for checking recursively if lifting is needed file | diff | annotate
Wed, 14 Oct 2009 09:50:13 +0200 Cezary Kaliszyk Merge file | diff | annotate
Wed, 14 Oct 2009 09:47:16 +0200 Cezary Kaliszyk Proper handling of non-lifted quantifiers, testing type freezing. file | diff | annotate
Tue, 13 Oct 2009 22:22:15 +0200 Christian Urban slight simplification of atomize_thm file | diff | annotate
Tue, 13 Oct 2009 18:01:54 +0200 Cezary Kaliszyk atomize_thm and meta_quantify. file | diff | annotate
Tue, 13 Oct 2009 13:37:07 +0200 Cezary Kaliszyk Regularizing HOL all. file | diff | annotate
Tue, 13 Oct 2009 11:38:35 +0200 Cezary Kaliszyk ":" is used for being in a set, "IN" means something else... file | diff | annotate
Tue, 13 Oct 2009 11:03:55 +0200 Cezary Kaliszyk First (untested) version of regularize for abstractions. file | diff | annotate
Mon, 12 Oct 2009 23:39:14 +0200 Christian Urban slightly modified the parser file | diff | annotate
Mon, 12 Oct 2009 23:16:20 +0200 Christian Urban deleted diagnostic code file | diff | annotate
Mon, 12 Oct 2009 23:06:14 +0200 Christian Urban added quotient command (you need to update isar-keywords-prove.el) file | diff | annotate
Mon, 12 Oct 2009 16:31:29 +0200 Cezary Kaliszyk Bounded quantifier file | diff | annotate
Mon, 12 Oct 2009 15:47:27 +0200 Cezary Kaliszyk The tyREL function. file | diff | annotate
Mon, 12 Oct 2009 14:30:50 +0200 Christian Urban started some strange functions file | diff | annotate
Mon, 12 Oct 2009 13:58:31 +0200 Cezary Kaliszyk Further with the manual proof file | diff | annotate
Fri, 09 Oct 2009 17:05:45 +0200 Cezary Kaliszyk Further experiments with proving induction manually file | diff | annotate
Fri, 09 Oct 2009 15:03:43 +0200 Cezary Kaliszyk Testing if I can prove the regularized version of induction manually file | diff | annotate
Thu, 08 Oct 2009 14:27:50 +0200 Christian Urban exported parts of QuotMain into a separate ML-file file | diff | annotate
Tue, 06 Oct 2009 15:11:30 +0200 Christian Urban consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar file | diff | annotate
Tue, 06 Oct 2009 11:56:23 +0200 Christian Urban simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier) file | diff | annotate
Tue, 06 Oct 2009 11:41:35 +0200 Christian Urban renamed unlam_def to unabs_def (matching the function abs_def in drule.ML) file | diff | annotate
Tue, 06 Oct 2009 11:36:08 +0200 Christian Urban tuned; nothing serious file | diff | annotate
Tue, 06 Oct 2009 09:28:59 +0200 Christian Urban another improvement to unlam_def file | diff | annotate
Tue, 06 Oct 2009 02:02:51 +0200 Christian Urban one further improvement to unlam_def file | diff | annotate
Tue, 06 Oct 2009 01:50:13 +0200 Christian Urban simplified the unlam_def function file | diff | annotate
Mon, 05 Oct 2009 11:54:02 +0200 Christian Urban added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types) file | diff | annotate
Mon, 05 Oct 2009 11:24:32 +0200 Christian Urban used prop_of to get the term of a theorem (replaces crep_thm) file | diff | annotate
Fri, 02 Oct 2009 11:10:21 +0200 Cezary Kaliszyk Merged file | diff | annotate
Fri, 02 Oct 2009 11:09:33 +0200 Cezary Kaliszyk First theorem with quantifiers. Learned how to use sledgehammer. file | diff | annotate
Thu, 01 Oct 2009 16:10:14 +0200 Christian Urban simplified the storage of the map-functions by using TheoryDataFun file | diff | annotate
Wed, 30 Sep 2009 16:57:09 +0200 Cezary Kaliszyk Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'. file | diff | annotate
Tue, 29 Sep 2009 22:35:48 +0200 Christian Urban used new cong_tac file | diff | annotate
Tue, 29 Sep 2009 17:46:18 +0200 Cezary Kaliszyk First version of handling of the universal quantifier file | diff | annotate
Tue, 29 Sep 2009 15:58:14 +0200 Cezary Kaliszyk Handling abstraction correctly. file | diff | annotate
Tue, 29 Sep 2009 13:38:27 +0200 Cezary Kaliszyk second test file | diff | annotate
Tue, 29 Sep 2009 13:24:57 +0200 Cezary Kaliszyk Test line file | diff | annotate
Tue, 29 Sep 2009 11:55:37 +0200 Cezary Kaliszyk Partially fix lifting of card_suc. The quantified variable still needs to be changed. file | diff | annotate
Tue, 29 Sep 2009 10:49:31 +0200 Cezary Kaliszyk Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests. file | diff | annotate
Tue, 29 Sep 2009 09:58:02 +0200 Cezary Kaliszyk Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues. file | diff | annotate
Tue, 29 Sep 2009 09:26:22 +0200 Cezary Kaliszyk Merged file | diff | annotate
Mon, 28 Sep 2009 19:24:55 +0200 Christian Urban consistent state file | diff | annotate
Mon, 28 Sep 2009 19:22:28 +0200 Christian Urban some tuning of my code file | diff | annotate
Mon, 28 Sep 2009 19:15:19 +0200 Cezary Kaliszyk Cleanup file | diff | annotate
Mon, 28 Sep 2009 19:10:27 +0200 Cezary Kaliszyk Merged file | diff | annotate
Mon, 28 Sep 2009 18:59:04 +0200 Cezary Kaliszyk Cleaning the code with Makarius file | diff | annotate
Mon, 28 Sep 2009 15:37:38 +0200 Cezary Kaliszyk Instnatiation with a schematic variable file | diff | annotate
Mon, 28 Sep 2009 02:39:44 +0200 Christian Urban added ctxt as explicit argument to build_goal; tuned file | diff | annotate
Fri, 25 Sep 2009 19:26:18 +0200 Christian Urban slightly tuned the comment for unlam file | diff | annotate
Fri, 25 Sep 2009 17:08:50 +0200 Christian Urban fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x file | diff | annotate
Fri, 25 Sep 2009 16:50:11 +0200 Christian Urban tuned slightly one proof file | diff | annotate
Fri, 25 Sep 2009 14:50:35 +0200 Cezary Kaliszyk A version of the tactic that exports variables correctly. file | diff | annotate
Fri, 25 Sep 2009 09:38:16 +0200 Cezary Kaliszyk Minor cleaning: whitespace, commas etc. file | diff | annotate
Thu, 24 Sep 2009 17:43:26 +0200 Cezary Kaliszyk Correctly handling abstractions while building goals file | diff | annotate
Thu, 24 Sep 2009 13:32:52 +0200 Cezary Kaliszyk Minor cleanup file | diff | annotate
Thu, 24 Sep 2009 11:38:20 +0200 Cezary Kaliszyk Found the source for the exception and added a handle for it. file | diff | annotate
Thu, 24 Sep 2009 09:09:46 +0200 Cezary Kaliszyk Make the tactic use Trueprop_cong and atomize. file | diff | annotate
Wed, 23 Sep 2009 16:57:56 +0200 Cezary Kaliszyk Proper code for getting the prop out of the theorem. file | diff | annotate
Wed, 23 Sep 2009 16:44:56 +0200 Cezary Kaliszyk Using "atomize" the versions with arbitrary Trueprops can be proven. file | diff | annotate
less more (0) -60 tip
nominal2