Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sun, 29 Jan 2006 19:23:44 +0100 CPure: Context.add_setup;
changeset
wenzelm [Sun, 29 Jan 2006 19:23:44 +0100] rev 18837
CPure: Context.add_setup;
Sun, 29 Jan 2006 19:23:43 +0100 tuned proofs;
changeset
wenzelm [Sun, 29 Jan 2006 19:23:43 +0100] rev 18836
tuned proofs;
Sun, 29 Jan 2006 19:23:42 +0100 implicit setup;
changeset
wenzelm [Sun, 29 Jan 2006 19:23:42 +0100] rev 18835
implicit setup;
Sun, 29 Jan 2006 19:23:41 +0100 default rule step: norm_hhf_tac;
changeset
wenzelm [Sun, 29 Jan 2006 19:23:41 +0100] rev 18834
default rule step: norm_hhf_tac;
Sun, 29 Jan 2006 19:23:40 +0100 tuned comment;
changeset
wenzelm [Sun, 29 Jan 2006 19:23:40 +0100] rev 18833
tuned comment;
Sun, 29 Jan 2006 19:23:38 +0100 declare 'defn' rules;
changeset
wenzelm [Sun, 29 Jan 2006 19:23:38 +0100] rev 18832
declare 'defn' rules;
Sat, 28 Jan 2006 17:29:49 +0100 LocalDefs;
changeset
wenzelm [Sat, 28 Jan 2006 17:29:49 +0100] rev 18831
LocalDefs;
Sat, 28 Jan 2006 17:29:06 +0100 Basic operations on local definitions.
changeset
wenzelm [Sat, 28 Jan 2006 17:29:06 +0100] rev 18830
Basic operations on local definitions.
Sat, 28 Jan 2006 17:29:04 +0100 removed unnecessary Syntax.fix_mixfix;
changeset
wenzelm [Sat, 28 Jan 2006 17:29:04 +0100] rev 18829
removed unnecessary Syntax.fix_mixfix;
Sat, 28 Jan 2006 17:29:03 +0100 added axiomatization_loc, definition_loc;
changeset
wenzelm [Sat, 28 Jan 2006 17:29:03 +0100] rev 18828
added axiomatization_loc, definition_loc; definition: let LocalDefs.derived_def do the actual work;
Sat, 28 Jan 2006 17:29:02 +0100 moved local defs to local_defs.ML;
changeset
wenzelm [Sat, 28 Jan 2006 17:29:02 +0100] rev 18827
moved local defs to local_defs.ML;
Sat, 28 Jan 2006 17:29:00 +0100 LocalDefs;
changeset
wenzelm [Sat, 28 Jan 2006 17:29:00 +0100] rev 18826
LocalDefs; unfolding(_i): support object-level rewrites;
Sat, 28 Jan 2006 17:28:59 +0100 removed unatomize;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:59 +0100] rev 18825
removed unatomize; added versions of meta_rewrite, unfold, fold;
Sat, 28 Jan 2006 17:28:58 +0100 (un)fold: support object-level rewrites;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:58 +0100] rev 18824
(un)fold: support object-level rewrites;
Sat, 28 Jan 2006 17:28:57 +0100 added print_consts;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:57 +0100] rev 18823
added print_consts; tuned;
Sat, 28 Jan 2006 17:28:56 +0100 removed obsolete keyword 'files';
changeset
wenzelm [Sat, 28 Jan 2006 17:28:56 +0100] rev 18822
removed obsolete keyword 'files';
Sat, 28 Jan 2006 17:28:55 +0100 (un)folded: support object-level rewrites;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:55 +0100] rev 18821
(un)folded: support object-level rewrites;
Sat, 28 Jan 2006 17:28:54 +0100 added equals_cong;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:54 +0100] rev 18820
added equals_cong;
Sat, 28 Jan 2006 17:28:53 +0100 added Isar/local_defs.ML;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:53 +0100] rev 18819
added Isar/local_defs.ML;
Sat, 28 Jan 2006 17:28:52 +0100 LocalDefs.add_def;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:52 +0100] rev 18818
LocalDefs.add_def;
Sat, 28 Jan 2006 17:28:51 +0100 LocalDefs.def_export;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:51 +0100] rev 18817
LocalDefs.def_export;
Sat, 28 Jan 2006 17:28:50 +0100 tuned proofs;
changeset
wenzelm [Sat, 28 Jan 2006 17:28:50 +0100] rev 18816
tuned proofs;
Sat, 28 Jan 2006 17:28:48 +0100 Pure/Isar: (un)folded, (un)fold, unfolding support
changeset
wenzelm [Sat, 28 Jan 2006 17:28:48 +0100] rev 18815
Pure/Isar: (un)folded, (un)fold, unfolding support object-level rewrite rules; ML/Isar: installed ML toplevel pretty printer for type Proof.context;
Fri, 27 Jan 2006 20:17:24 +0100 interrupt_timeout for Poly replaced by stub
changeset
webertj [Fri, 27 Jan 2006 20:17:24 +0100] rev 18814
interrupt_timeout for Poly replaced by stub
Fri, 27 Jan 2006 19:05:24 +0100 added atomize_iff;
changeset
wenzelm [Fri, 27 Jan 2006 19:05:24 +0100] rev 18813
added atomize_iff;
Fri, 27 Jan 2006 19:03:19 +0100 renamed Pretty.gen_list to Pretty.enum;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:19 +0100] rev 18812
renamed Pretty.gen_list to Pretty.enum;
Fri, 27 Jan 2006 19:03:17 +0100 swapped theory_context;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:17 +0100] rev 18811
swapped theory_context;
Fri, 27 Jan 2006 19:03:16 +0100 swapped Toplevel.theory_context;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:16 +0100] rev 18810
swapped Toplevel.theory_context; definition(_i): actually rulify as well, support more of object-logic; definition(_i): more precise treatment of local fixes;
Fri, 27 Jan 2006 19:03:15 +0100 added invent_fixes;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:15 +0100] rev 18809
added invent_fixes; added debug flag, pprint_context;
Fri, 27 Jan 2006 19:03:14 +0100 swapped Toplevel.theory_context;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:14 +0100] rev 18808
swapped Toplevel.theory_context; tuned;
Fri, 27 Jan 2006 19:03:13 +0100 renamed reverse_atomize to unatomize;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:13 +0100] rev 18807
renamed reverse_atomize to unatomize; added rulify_term/tac;
Fri, 27 Jan 2006 19:03:12 +0100 init: include view;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:12 +0100] rev 18806
init: include view; swapped Toplevel.theory_context; removed obsolete smart_note_thmss; moved note_thmss_qualified to PureThy; unified code of note_thmss(_i), add_thmss, locale_results;
Fri, 27 Jan 2006 19:03:11 +0100 improved 'notes', including proper treatment of locale results;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:11 +0100] rev 18805
improved 'notes', including proper treatment of locale results; tuned;
Fri, 27 Jan 2006 19:03:10 +0100 swapped Toplevel.theory_context;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:10 +0100] rev 18804
swapped Toplevel.theory_context;
Fri, 27 Jan 2006 19:03:09 +0100 Locale.init;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:09 +0100] rev 18803
Locale.init;
Fri, 27 Jan 2006 19:03:08 +0100 renamed gen_list to enum;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:08 +0100] rev 18802
renamed gen_list to enum; added separate; tuned;
Fri, 27 Jan 2006 19:03:07 +0100 moved theorem tags from Drule to PureThy;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:07 +0100] rev 18801
moved theorem tags from Drule to PureThy; replaced kind attribute by kind string; tuned name_multi: index > 1 only; added note_thmss_qualified (from Isar/locale.ML);
Fri, 27 Jan 2006 19:03:05 +0100 added ProofContext.pprint_context (depends on ProofContext.debug);
changeset
wenzelm [Fri, 27 Jan 2006 19:03:05 +0100] rev 18800
added ProofContext.pprint_context (depends on ProofContext.debug);
Fri, 27 Jan 2006 19:03:02 +0100 moved theorem tags from Drule to PureThy;
changeset
wenzelm [Fri, 27 Jan 2006 19:03:02 +0100] rev 18799
moved theorem tags from Drule to PureThy;
Fri, 27 Jan 2006 18:29:33 +0100 tidying up SPASS output
changeset
paulson [Fri, 27 Jan 2006 18:29:33 +0100] rev 18798
tidying up SPASS output
Fri, 27 Jan 2006 18:29:11 +0100 tidying
changeset
paulson [Fri, 27 Jan 2006 18:29:11 +0100] rev 18797
tidying
Fri, 27 Jan 2006 18:28:55 +0100 better reporting
changeset
paulson [Fri, 27 Jan 2006 18:28:55 +0100] rev 18796
better reporting
Fri, 27 Jan 2006 16:05:23 +0100 Interface to access the specification of a named locale.
changeset
ballarin [Fri, 27 Jan 2006 16:05:23 +0100] rev 18795
Interface to access the specification of a named locale.
Fri, 27 Jan 2006 05:46:39 +0100 Added new file Tools/ATP/reduce_axiomsN.ML
changeset
mengj [Fri, 27 Jan 2006 05:46:39 +0100] rev 18794
Added new file Tools/ATP/reduce_axiomsN.ML
Fri, 27 Jan 2006 05:45:25 +0100 Added in new file Tools/ATP/reduce_axiomsN.ML
changeset
mengj [Fri, 27 Jan 2006 05:45:25 +0100] rev 18793
Added in new file Tools/ATP/reduce_axiomsN.ML
Fri, 27 Jan 2006 05:37:12 +0100 Changed codes that call relevance filter.
changeset
mengj [Fri, 27 Jan 2006 05:37:12 +0100] rev 18792
Changed codes that call relevance filter.
Fri, 27 Jan 2006 05:34:20 +0100 Relevance filtering. Has replaced the previous version.
changeset
mengj [Fri, 27 Jan 2006 05:34:20 +0100] rev 18791
Relevance filtering. Has replaced the previous version.
Thu, 26 Jan 2006 20:42:15 +0100 interrupt_timeout now raises Interrupt instead of SML90.Interrupt
changeset
webertj [Thu, 26 Jan 2006 20:42:15 +0100] rev 18790
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
Thu, 26 Jan 2006 20:17:54 +0100 smaller example to prevent timeout
changeset
webertj [Thu, 26 Jan 2006 20:17:54 +0100] rev 18789
smaller example to prevent timeout
Thu, 26 Jan 2006 17:58:01 +0100 Fixed bug in code generator for primitive definitions that
changeset
berghofe [Thu, 26 Jan 2006 17:58:01 +0100] rev 18788
Fixed bug in code generator for primitive definitions that caused dependencies to get mixed up.
Thu, 26 Jan 2006 15:37:14 +0100 Inductive sets with no introduction rules are now allowed as well.
changeset
berghofe [Thu, 26 Jan 2006 15:37:14 +0100] rev 18787
Inductive sets with no introduction rules are now allowed as well.
Wed, 25 Jan 2006 00:21:44 +0100 added definition(_i);
changeset
wenzelm [Wed, 25 Jan 2006 00:21:44 +0100] rev 18786
added definition(_i);
Wed, 25 Jan 2006 00:21:43 +0100 renamed export to export_standard (again!), because it includes Drule.local_standard';
changeset
wenzelm [Wed, 25 Jan 2006 00:21:43 +0100] rev 18785
renamed export to export_standard (again!), because it includes Drule.local_standard'; added abs_def (from locale.ML);
Wed, 25 Jan 2006 00:21:42 +0100 ProofContext.export_standard;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:42 +0100] rev 18784
ProofContext.export_standard;
Wed, 25 Jan 2006 00:21:41 +0100 tuned atomize_cterm;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:41 +0100] rev 18783
tuned atomize_cterm; added reverse_atomize_term/tac;
Wed, 25 Jan 2006 00:21:40 +0100 turned abstract_term into ProofContext.abs_def;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:40 +0100] rev 18782
turned abstract_term into ProofContext.abs_def; ProofContext.export_standard;
Wed, 25 Jan 2006 00:21:39 +0100 added constant definition;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:39 +0100] rev 18781
added constant definition; tuned interfaces; tuned;
Wed, 25 Jan 2006 00:21:38 +0100 added 'definition';
changeset
wenzelm [Wed, 25 Jan 2006 00:21:38 +0100] rev 18780
added 'definition'; 'spezification': optional fixes;
Wed, 25 Jan 2006 00:21:37 +0100 tuned comment;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:37 +0100] rev 18779
tuned comment;
Wed, 25 Jan 2006 00:21:36 +0100 export name_multi;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:36 +0100] rev 18778
export name_multi;
Wed, 25 Jan 2006 00:21:35 +0100 abs_def: improved error;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:35 +0100] rev 18777
abs_def: improved error;
Wed, 25 Jan 2006 00:21:34 +0100 ObjectLogic.atomize_cterm;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:34 +0100] rev 18776
ObjectLogic.atomize_cterm;
Wed, 25 Jan 2006 00:21:32 +0100 updated;
changeset
wenzelm [Wed, 25 Jan 2006 00:21:32 +0100] rev 18775
updated;
Tue, 24 Jan 2006 15:16:06 +0100 works with DPLL solver now
changeset
webertj [Tue, 24 Jan 2006 15:16:06 +0100] rev 18774
works with DPLL solver now
Tue, 24 Jan 2006 13:28:06 +0100 the additional freshness-condition in the one-induction
changeset
urbanc [Tue, 24 Jan 2006 13:28:06 +0100] rev 18773
the additional freshness-condition in the one-induction is not needed anywhere.
Tue, 24 Jan 2006 00:44:39 +0100 fixed code_generate syntax;
changeset
wenzelm [Tue, 24 Jan 2006 00:44:39 +0100] rev 18772
fixed code_generate syntax;
Tue, 24 Jan 2006 00:43:34 +0100 renamed axiomatize(_i) to axiomatization(_i);
changeset
wenzelm [Tue, 24 Jan 2006 00:43:34 +0100] rev 18771
renamed axiomatize(_i) to axiomatization(_i); LocalTheory;
Tue, 24 Jan 2006 00:43:33 +0100 renamed inferred_type to inferred_param;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:33 +0100] rev 18770
renamed inferred_type to inferred_param; added inferred_fixes;
Tue, 24 Jan 2006 00:43:32 +0100 ProofContext.inferred_param;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:32 +0100] rev 18769
ProofContext.inferred_param;
Tue, 24 Jan 2006 00:43:31 +0100 removed the_params;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:31 +0100] rev 18768
removed the_params;
Tue, 24 Jan 2006 00:43:29 +0100 added actual operations;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:29 +0100] rev 18767
added actual operations;
Tue, 24 Jan 2006 00:43:28 +0100 axiomatization: optional vars;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:28 +0100] rev 18766
axiomatization: optional vars;
Tue, 24 Jan 2006 00:43:27 +0100 LocalTheory.pretty_consts;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:27 +0100] rev 18765
LocalTheory.pretty_consts;
Tue, 24 Jan 2006 00:43:25 +0100 tuned;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:25 +0100] rev 18764
tuned;
Tue, 24 Jan 2006 00:43:24 +0100 add_finals: prep_consts, i.e. varify type;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:24 +0100] rev 18763
add_finals: prep_consts, i.e. varify type;
Tue, 24 Jan 2006 00:43:23 +0100 added dest_all;
changeset
wenzelm [Tue, 24 Jan 2006 00:43:23 +0100] rev 18762
added dest_all;
Mon, 23 Jan 2006 18:20:48 +0100 TimeLimit replaced by interrupt_timeout
changeset
webertj [Mon, 23 Jan 2006 18:20:48 +0100] rev 18761
TimeLimit replaced by interrupt_timeout
Mon, 23 Jan 2006 17:29:52 +0100 TimeLimit replaced by interrupt_timeout
changeset
webertj [Mon, 23 Jan 2006 17:29:52 +0100] rev 18760
TimeLimit replaced by interrupt_timeout
Mon, 23 Jan 2006 15:23:31 +0100 Updated to Isabelle 2006-01-23
changeset
krauss [Mon, 23 Jan 2006 15:23:31 +0100] rev 18759
Updated to Isabelle 2006-01-23
Mon, 23 Jan 2006 15:14:06 +0100 made change for ex1
changeset
urbanc [Mon, 23 Jan 2006 15:14:06 +0100] rev 18758
made change for ex1
Mon, 23 Jan 2006 14:07:52 +0100 removed problematic keyword 'atom'
changeset
haftmann [Mon, 23 Jan 2006 14:07:52 +0100] rev 18757
removed problematic keyword 'atom'
Mon, 23 Jan 2006 14:06:40 +0100 more general serializer
changeset
haftmann [Mon, 23 Jan 2006 14:06:40 +0100] rev 18756
more general serializer
Mon, 23 Jan 2006 14:06:28 +0100 slight steps forward
changeset
haftmann [Mon, 23 Jan 2006 14:06:28 +0100] rev 18755
slight steps forward
Mon, 23 Jan 2006 14:06:11 +0100 exported after_qed for axclass instance
changeset
haftmann [Mon, 23 Jan 2006 14:06:11 +0100] rev 18754
exported after_qed for axclass instance
Mon, 23 Jan 2006 11:41:54 +0100 ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
changeset
paulson [Mon, 23 Jan 2006 11:41:54 +0100] rev 18753
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
Mon, 23 Jan 2006 11:38:43 +0100 Clausification now handles some IFs in rewrite rules (if-split did not work)
changeset
paulson [Mon, 23 Jan 2006 11:38:43 +0100] rev 18752
Clausification now handles some IFs in rewrite rules (if-split did not work)
Mon, 23 Jan 2006 11:37:53 +0100 bugfix: induct_tac no longer raises THM "dest_state"
changeset
paulson [Mon, 23 Jan 2006 11:37:53 +0100] rev 18751
bugfix: induct_tac no longer raises THM "dest_state"
Mon, 23 Jan 2006 11:36:50 +0100 fixed the <<= notation
changeset
paulson [Mon, 23 Jan 2006 11:36:50 +0100] rev 18750
fixed the <<= notation
Mon, 23 Jan 2006 11:36:05 +0100 replacement of bool by a datatype (making problems first-order). More lemma names
changeset
paulson [Mon, 23 Jan 2006 11:36:05 +0100] rev 18749
replacement of bool by a datatype (making problems first-order). More lemma names
Mon, 23 Jan 2006 10:34:38 +0100 Fixed a bug.
changeset
mengj [Mon, 23 Jan 2006 10:34:38 +0100] rev 18748
Fixed a bug.
Sun, 22 Jan 2006 22:16:34 +0100 no essential changes
changeset
urbanc [Sun, 22 Jan 2006 22:16:34 +0100] rev 18747
no essential changes
Sun, 22 Jan 2006 22:11:50 +0100 made the change for setup-functions not returning functions
changeset
urbanc [Sun, 22 Jan 2006 22:11:50 +0100] rev 18746
made the change for setup-functions not returning functions anymore
Sun, 22 Jan 2006 21:58:43 +0100 a fixme comments about abs_fun_if, which should be called perm_if
changeset
urbanc [Sun, 22 Jan 2006 21:58:43 +0100] rev 18745
a fixme comments about abs_fun_if, which should be called perm_if and moved to the "bool"-section
Sun, 22 Jan 2006 18:46:01 +0100 Local theory operations, with optional target locale.
changeset
wenzelm [Sun, 22 Jan 2006 18:46:01 +0100] rev 18744
Local theory operations, with optional target locale.
Sun, 22 Jan 2006 18:46:00 +0100 added restore_body;
changeset
wenzelm [Sun, 22 Jan 2006 18:46:00 +0100] rev 18743
added restore_body;
Sun, 22 Jan 2006 18:45:59 +0100 added the_params;
changeset
wenzelm [Sun, 22 Jan 2006 18:45:59 +0100] rev 18742
added the_params;
(0) -10000 -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle