Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tue, 06 Jul 1999 21:03:57 +0200 export term_of_typ;
changeset
wenzelm [Tue, 06 Jul 1999 21:03:57 +0200] rev 6901
export term_of_typ;
Tue, 06 Jul 1999 21:03:34 +0200 begin_theory: disallow finished;
changeset
wenzelm [Tue, 06 Jul 1999 21:03:34 +0200] rev 6900
begin_theory: disallow finished;
Tue, 06 Jul 1999 21:03:03 +0200 added clear_mss;
changeset
wenzelm [Tue, 06 Jul 1999 21:03:03 +0200] rev 6899
added clear_mss;
Mon, 05 Jul 1999 09:52:25 +0200 variant version;
changeset
wenzelm [Mon, 05 Jul 1999 09:52:25 +0200] rev 6898
variant version;
Sun, 04 Jul 1999 20:21:45 +0200 fixed scope of x:??H;
changeset
wenzelm [Sun, 04 Jul 1999 20:21:45 +0200] rev 6897
fixed scope of x:??H; improved final reasoning: fully formal now;
Sun, 04 Jul 1999 20:20:36 +0200 close_block: transfer_used_names;
changeset
wenzelm [Sun, 04 Jul 1999 20:20:36 +0200] rev 6896
close_block: transfer_used_names; tuned;
Sun, 04 Jul 1999 20:19:28 +0200 added transfer_used_names;
changeset
wenzelm [Sun, 04 Jul 1999 20:19:28 +0200] rev 6895
added transfer_used_names;
Sat, 03 Jul 1999 00:40:57 +0200 oops;
changeset
wenzelm [Sat, 03 Jul 1999 00:40:57 +0200] rev 6894
oops;
Sat, 03 Jul 1999 00:28:05 +0200 proper text;
changeset
wenzelm [Sat, 03 Jul 1999 00:28:05 +0200] rev 6893
proper text;
Sat, 03 Jul 1999 00:26:00 +0200 tuned;
changeset
wenzelm [Sat, 03 Jul 1999 00:26:00 +0200] rev 6892
tuned;
Sat, 03 Jul 1999 00:23:17 +0200 tuned print_state;
changeset
wenzelm [Sat, 03 Jul 1999 00:23:17 +0200] rev 6891
tuned print_state;
Sat, 03 Jul 1999 00:22:53 +0200 fixed 'txt';
changeset
wenzelm [Sat, 03 Jul 1999 00:22:53 +0200] rev 6890
fixed 'txt';
Sat, 03 Jul 1999 00:21:35 +0200 pretty_thm: include oracles (!) in hyps;
changeset
wenzelm [Sat, 03 Jul 1999 00:21:35 +0200] rev 6889
pretty_thm: include oracles (!) in hyps;
Fri, 02 Jul 1999 19:04:32 +0200 skip_proof feature 'sorry' (for quick_and_dirty mode only);
changeset
wenzelm [Fri, 02 Jul 1999 19:04:32 +0200] rev 6888
skip_proof feature 'sorry' (for quick_and_dirty mode only);
Fri, 02 Jul 1999 15:05:16 +0200 generalized fixes get index 0;
changeset
wenzelm [Fri, 02 Jul 1999 15:05:16 +0200] rev 6887
generalized fixes get index 0;
Fri, 02 Jul 1999 15:04:45 +0200 added 'txt';
changeset
wenzelm [Fri, 02 Jul 1999 15:04:45 +0200] rev 6886
added 'txt';
Fri, 02 Jul 1999 15:04:31 +0200 add_txt;
changeset
wenzelm [Fri, 02 Jul 1999 15:04:31 +0200] rev 6885
add_txt;
Fri, 02 Jul 1999 15:04:12 +0200 tuned;
changeset
wenzelm [Fri, 02 Jul 1999 15:04:12 +0200] rev 6884
tuned;
Thu, 01 Jul 1999 22:20:58 +0200 fixed order_trans;
changeset
wenzelm [Thu, 01 Jul 1999 22:20:58 +0200] rev 6883
fixed order_trans;
Thu, 01 Jul 1999 21:30:18 +0200 added KnasterTarski.thy;
changeset
wenzelm [Thu, 01 Jul 1999 21:30:18 +0200] rev 6882
added KnasterTarski.thy;
Thu, 01 Jul 1999 21:29:53 +0200 renamed with/APP to of/OF;
changeset
wenzelm [Thu, 01 Jul 1999 21:29:53 +0200] rev 6881
renamed with/APP to of/OF;
Thu, 01 Jul 1999 21:28:49 +0200 Isar_examples/KnasterTarski.thy;
changeset
wenzelm [Thu, 01 Jul 1999 21:28:49 +0200] rev 6880
Isar_examples/KnasterTarski.thy;
Thu, 01 Jul 1999 21:27:46 +0200 added with_facts(_i);
changeset
wenzelm [Thu, 01 Jul 1999 21:27:46 +0200] rev 6879
added with_facts(_i); also, finally: opt_rules;
Thu, 01 Jul 1999 21:27:04 +0200 'with' as == 'from' as facts;
changeset
wenzelm [Thu, 01 Jul 1999 21:27:04 +0200] rev 6878
'with' as == 'from' as facts; also, finally: opt_rules;
Thu, 01 Jul 1999 21:25:58 +0200 also, finally: opt_rules;
changeset
wenzelm [Thu, 01 Jul 1999 21:25:58 +0200] rev 6877
also, finally: opt_rules;
Thu, 01 Jul 1999 21:20:57 +0200 have_thmss: more_ths;
changeset
wenzelm [Thu, 01 Jul 1999 21:20:57 +0200] rev 6876
have_thmss: more_ths; simple_have_thmss;
Thu, 01 Jul 1999 21:20:27 +0200 have_thmss: more_ths;
changeset
wenzelm [Thu, 01 Jul 1999 21:20:27 +0200] rev 6875
have_thmss: more_ths;
Thu, 01 Jul 1999 21:19:45 +0200 renamed with/APP to of/OF;
changeset
wenzelm [Thu, 01 Jul 1999 21:19:45 +0200] rev 6874
renamed with/APP to of/OF;
Thu, 01 Jul 1999 17:42:27 +0200 tuned;
changeset
wenzelm [Thu, 01 Jul 1999 17:42:27 +0200] rev 6873
tuned;
Thu, 01 Jul 1999 17:41:16 +0200 fixed backtracking of global_qed;
changeset
wenzelm [Thu, 01 Jul 1999 17:41:16 +0200] rev 6872
fixed backtracking of global_qed;
Thu, 01 Jul 1999 17:40:48 +0200 added check_result;
changeset
wenzelm [Thu, 01 Jul 1999 17:40:48 +0200] rev 6871
added check_result; setmp Display.show_hyps false; fixed auto_bind_facts; tuned finish_proof; fixed backtracking of global_qed;
Thu, 01 Jul 1999 17:38:44 +0200 setmp Display.show_hyps false;
changeset
wenzelm [Thu, 01 Jul 1999 17:38:44 +0200] rev 6870
setmp Display.show_hyps false;
Thu, 01 Jul 1999 17:24:29 +0200 fix, assume, presume: prf_asm;
changeset
wenzelm [Thu, 01 Jul 1999 17:24:29 +0200] rev 6869
fix, assume, presume: prf_asm;
Thu, 01 Jul 1999 17:24:14 +0200 added prf_asm;
changeset
wenzelm [Thu, 01 Jul 1999 17:24:14 +0200] rev 6868
added prf_asm;
Thu, 01 Jul 1999 10:36:38 +0200 expandshort
changeset
paulson [Thu, 01 Jul 1999 10:36:38 +0200] rev 6867
expandshort
Thu, 01 Jul 1999 10:35:35 +0200 many new theorems concerning multiplication and (in)equations
changeset
paulson [Thu, 01 Jul 1999 10:35:35 +0200] rev 6866
many new theorems concerning multiplication and (in)equations
Thu, 01 Jul 1999 10:33:50 +0200 now div and mod are overloaded; dvd is polymorphic
changeset
paulson [Thu, 01 Jul 1999 10:33:50 +0200] rev 6865
now div and mod are overloaded; dvd is polymorphic
Thu, 01 Jul 1999 10:32:57 +0200 new laws mult_le_cancel1, mult_le_cancel2
changeset
paulson [Thu, 01 Jul 1999 10:32:57 +0200] rev 6864
new laws mult_le_cancel1, mult_le_cancel2
Wed, 30 Jun 1999 16:00:06 +0200 antisym first;
changeset
wenzelm [Wed, 30 Jun 1999 16:00:06 +0200] rev 6863
antisym first;
Wed, 30 Jun 1999 13:42:47 +0200 more robust trans rules;
changeset
wenzelm [Wed, 30 Jun 1999 13:42:47 +0200] rev 6862
more robust trans rules;
Wed, 30 Jun 1999 12:24:32 +0200 Isar.sync_main;
changeset
wenzelm [Wed, 30 Jun 1999 12:24:32 +0200] rev 6861
Isar.sync_main;
Wed, 30 Jun 1999 12:23:46 +0200 added sync;
changeset
wenzelm [Wed, 30 Jun 1999 12:23:46 +0200] rev 6860
added sync;
Wed, 30 Jun 1999 12:23:34 +0200 sync token;
changeset
wenzelm [Wed, 30 Jun 1999 12:23:34 +0200] rev 6859
sync token;
Wed, 30 Jun 1999 12:22:45 +0200 sync;
changeset
wenzelm [Wed, 30 Jun 1999 12:22:45 +0200] rev 6858
sync;
Wed, 30 Jun 1999 12:22:31 +0200 added sync marker;
changeset
wenzelm [Wed, 30 Jun 1999 12:22:31 +0200] rev 6857
added sync marker;
Wed, 30 Jun 1999 09:47:16 +0200 New thm trancl_trans_induct
changeset
nipkow [Wed, 30 Jun 1999 09:47:16 +0200] rev 6856
New thm trancl_trans_induct
Tue, 29 Jun 1999 11:58:21 +0200 Bad translation fixed.
changeset
nipkow [Tue, 29 Jun 1999 11:58:21 +0200] rev 6855
Bad translation fixed.
Mon, 28 Jun 1999 23:05:19 +0200 updated;
changeset
wenzelm [Mon, 28 Jun 1999 23:05:19 +0200] rev 6854
updated;
Mon, 28 Jun 1999 23:02:38 +0200 improved RANGE;
changeset
wenzelm [Mon, 28 Jun 1999 23:02:38 +0200] rev 6853
improved RANGE;
Mon, 28 Jun 1999 23:02:03 +0200 tuned;
changeset
wenzelm [Mon, 28 Jun 1999 23:02:03 +0200] rev 6852
tuned;
Mon, 28 Jun 1999 21:48:36 +0200 cond_extern_table;
changeset
wenzelm [Mon, 28 Jun 1999 21:48:36 +0200] rev 6851
cond_extern_table;
Mon, 28 Jun 1999 21:47:55 +0200 added presume command;
changeset
wenzelm [Mon, 28 Jun 1999 21:47:55 +0200] rev 6850
added presume command;
Mon, 28 Jun 1999 21:47:04 +0200 cond_extern_table;
changeset
wenzelm [Mon, 28 Jun 1999 21:47:04 +0200] rev 6849
cond_extern_table; datatype method = Method of thm list -> tactic;
Mon, 28 Jun 1999 21:46:33 +0200 tuned print_state;
changeset
wenzelm [Mon, 28 Jun 1999 21:46:33 +0200] rev 6848
tuned print_state; datatype method = Method of thm list -> tactic; assumptions: back-pressure solver as parameter;
Mon, 28 Jun 1999 21:44:19 +0200 tuned output: print_context replaced by strings_of_context;
changeset
wenzelm [Mon, 28 Jun 1999 21:44:19 +0200] rev 6847
tuned output: print_context replaced by strings_of_context; assumptions: back-pressure solver as parameter;
Mon, 28 Jun 1999 21:41:02 +0200 cond_extern_table;
changeset
wenzelm [Mon, 28 Jun 1999 21:41:02 +0200] rev 6846
cond_extern_table;
Mon, 28 Jun 1999 21:38:50 +0200 added cond_extern_table;
changeset
wenzelm [Mon, 28 Jun 1999 21:38:50 +0200] rev 6845
added cond_extern_table;
Fri, 25 Jun 1999 13:37:51 +0200 branching_level = 400;
changeset
wenzelm [Fri, 25 Jun 1999 13:37:51 +0200] rev 6844
branching_level = 400;
Wed, 23 Jun 1999 10:40:13 +0200 tidied
changeset
paulson [Wed, 23 Jun 1999 10:40:13 +0200] rev 6843
tidied
Wed, 23 Jun 1999 10:39:35 +0200 renamed PPI to plam
changeset
paulson [Wed, 23 Jun 1999 10:39:35 +0200] rev 6842
renamed PPI to plam simplified the definition of lift_act
Wed, 23 Jun 1999 10:38:49 +0200 renamed PPI to plam
changeset
paulson [Wed, 23 Jun 1999 10:38:49 +0200] rev 6841
renamed PPI to plam
Wed, 23 Jun 1999 10:38:09 +0200 another non-working snapshot
changeset
paulson [Wed, 23 Jun 1999 10:38:09 +0200] rev 6840
another non-working snapshot
Wed, 23 Jun 1999 10:37:29 +0200 new distributive laws involving * and -
changeset
paulson [Wed, 23 Jun 1999 10:37:29 +0200] rev 6839
new distributive laws involving * and -
Wed, 23 Jun 1999 10:36:59 +0200 rewrite rules to distribute CONSTANT multiplication over sum and difference;
changeset
paulson [Wed, 23 Jun 1999 10:36:59 +0200] rev 6838
rewrite rules to distribute CONSTANT multiplication over sum and difference; removed automatic rewriting of 2x to x+x
Thu, 17 Jun 1999 10:43:05 +0200 another snapshot, still not working
changeset
paulson [Thu, 17 Jun 1999 10:43:05 +0200] rev 6837
another snapshot, still not working
Thu, 17 Jun 1999 10:41:39 +0200 new results about SKIP
changeset
paulson [Thu, 17 Jun 1999 10:41:39 +0200] rev 6836
new results about SKIP
Thu, 17 Jun 1999 10:39:30 +0200 addition of drop_... operators with new results and simplification of old ones
changeset
paulson [Thu, 17 Jun 1999 10:39:30 +0200] rev 6835
addition of drop_... operators with new results and simplification of old ones
Thu, 17 Jun 1999 10:36:03 +0200 renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
changeset
paulson [Thu, 17 Jun 1999 10:36:03 +0200] rev 6834
renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
Thu, 17 Jun 1999 10:35:01 +0200 many new guarantees laws
changeset
paulson [Thu, 17 Jun 1999 10:35:01 +0200] rev 6833
many new guarantees laws
Thu, 17 Jun 1999 10:34:23 +0200 moved image_UNION to Fun/image_UN
changeset
paulson [Thu, 17 Jun 1999 10:34:23 +0200] rev 6832
moved image_UNION to Fun/image_UN
Thu, 17 Jun 1999 10:33:43 +0200 expandshort
changeset
paulson [Thu, 17 Jun 1999 10:33:43 +0200] rev 6831
expandshort
Thu, 17 Jun 1999 10:33:33 +0200 renamed UNION_... to UN_... (to fit the convention)
changeset
paulson [Thu, 17 Jun 1999 10:33:33 +0200] rev 6830
renamed UNION_... to UN_... (to fit the convention)
Thu, 17 Jun 1999 10:32:52 +0200 renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
changeset
paulson [Thu, 17 Jun 1999 10:32:52 +0200] rev 6829
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT
Sun, 13 Jun 1999 13:57:31 +0200 not working but taking shape
changeset
paulson [Sun, 13 Jun 1999 13:57:31 +0200] rev 6828
not working but taking shape
Sun, 13 Jun 1999 13:56:12 +0200 guar; locale for the spec
changeset
paulson [Sun, 13 Jun 1999 13:56:12 +0200] rev 6827
guar; locale for the spec
Sun, 13 Jun 1999 13:55:28 +0200 many new results for reachable and lift_prog
changeset
paulson [Sun, 13 Jun 1999 13:55:28 +0200] rev 6826
many new results for reachable and lift_prog
Sun, 13 Jun 1999 13:54:56 +0200 new finiteness theorems
changeset
paulson [Sun, 13 Jun 1999 13:54:56 +0200] rev 6825
new finiteness theorems
Sun, 13 Jun 1999 13:54:34 +0200 renamed pfix_[lg}e
changeset
paulson [Sun, 13 Jun 1999 13:54:34 +0200] rev 6824
renamed pfix_[lg}e
Sun, 13 Jun 1999 13:53:33 +0200 new-style infix directives
changeset
paulson [Sun, 13 Jun 1999 13:53:33 +0200] rev 6823
new-style infix directives
Sun, 13 Jun 1999 13:52:50 +0200 guarantees -> guar
changeset
paulson [Sun, 13 Jun 1999 13:52:50 +0200] rev 6822
guarantees -> guar
Sun, 13 Jun 1999 13:52:26 +0200 guarantees -> juar
changeset
paulson [Sun, 13 Jun 1999 13:52:26 +0200] rev 6821
guarantees -> juar
Fri, 11 Jun 1999 17:14:00 +0200 rev=rev lemma.
changeset
nipkow [Fri, 11 Jun 1999 17:14:00 +0200] rev 6820
rev=rev lemma.
Fri, 11 Jun 1999 10:35:55 +0200 fixed title line; added spacing
changeset
paulson [Fri, 11 Jun 1999 10:35:55 +0200] rev 6819
fixed title line; added spacing
Fri, 11 Jun 1999 10:34:20 +0200 no longer needs ../Lex
changeset
paulson [Fri, 11 Jun 1999 10:34:20 +0200] rev 6818
no longer needs ../Lex
Fri, 11 Jun 1999 10:33:43 +0200 new UNITY files
changeset
paulson [Fri, 11 Jun 1999 10:33:43 +0200] rev 6817
new UNITY files
Thu, 10 Jun 1999 16:46:59 +0200 unclosed comment.
changeset
nipkow [Thu, 10 Jun 1999 16:46:59 +0200] rev 6816
unclosed comment.
Thu, 10 Jun 1999 12:36:19 +0200 The Allocator example: specifications
changeset
paulson [Thu, 10 Jun 1999 12:36:19 +0200] rev 6815
The Allocator example: specifications
Thu, 10 Jun 1999 10:50:19 +0200 expandshort
changeset
paulson [Thu, 10 Jun 1999 10:50:19 +0200] rev 6814
expandshort
Thu, 10 Jun 1999 10:41:36 +0200 many new lemmas about take & drop, incl the famous take-lemma
changeset
paulson [Thu, 10 Jun 1999 10:41:36 +0200] rev 6813
many new lemmas about take & drop, incl the famous take-lemma Ran expandshort
Thu, 10 Jun 1999 10:40:57 +0200 moved predicates refl, sym down to Relation.thy
changeset
paulson [Thu, 10 Jun 1999 10:40:57 +0200] rev 6812
moved predicates refl, sym down to Relation.thy
Thu, 10 Jun 1999 10:39:38 +0200 Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra
changeset
paulson [Thu, 10 Jun 1999 10:39:38 +0200] rev 6811
Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra
Thu, 10 Jun 1999 10:38:41 +0200 using the new GenPrefix theory
changeset
paulson [Thu, 10 Jun 1999 10:38:41 +0200] rev 6810
using the new GenPrefix theory
Thu, 10 Jun 1999 10:38:11 +0200 shortened Follows to Fols
changeset
paulson [Thu, 10 Jun 1999 10:38:11 +0200] rev 6809
shortened Follows to Fols
Thu, 10 Jun 1999 10:37:29 +0200 tidied
changeset
paulson [Thu, 10 Jun 1999 10:37:29 +0200] rev 6808
tidied
Thu, 10 Jun 1999 10:36:41 +0200 new translation to allow images over Nonce
changeset
paulson [Thu, 10 Jun 1999 10:36:41 +0200] rev 6807
new translation to allow images over Nonce
Thu, 10 Jun 1999 10:35:58 +0200 new preficates refl, sym [from Integ/Equiv], antisym
changeset
paulson [Thu, 10 Jun 1999 10:35:58 +0200] rev 6806
new preficates refl, sym [from Integ/Equiv], antisym
Thu, 10 Jun 1999 10:34:55 +0200 new lemma less_Suc_eq_0_disj
changeset
paulson [Thu, 10 Jun 1999 10:34:55 +0200] rev 6805
new lemma less_Suc_eq_0_disj
Thu, 10 Jun 1999 10:24:32 +0200 Generalized prefix theory, replacing the reference to directory Lex.
changeset
paulson [Thu, 10 Jun 1999 10:24:32 +0200] rev 6804
Generalized prefix theory, replacing the reference to directory Lex.
Wed, 09 Jun 1999 12:02:31 +0200 Stefan Merz's lemmas.
changeset
nipkow [Wed, 09 Jun 1999 12:02:31 +0200] rev 6803
Stefan Merz's lemmas.
Tue, 08 Jun 1999 12:53:20 +0200 added square root example.
changeset
nipkow [Tue, 08 Jun 1999 12:53:20 +0200] rev 6802
added square root example.
Tue, 08 Jun 1999 10:59:02 +0200 renamed the underlying relation of leadsTo from "leadsto"
changeset
paulson [Tue, 08 Jun 1999 10:59:02 +0200] rev 6801
renamed the underlying relation of leadsTo from "leadsto" to "leads" to reduce the risk of confusion
Tue, 08 Jun 1999 10:30:04 +0200 removed obsolete "Prefix" ancestor
changeset
paulson [Tue, 08 Jun 1999 10:30:04 +0200] rev 6800
removed obsolete "Prefix" ancestor
Tue, 08 Jun 1999 10:25:12 +0200 new classical example from Lewis Carroll via S G Pulman
changeset
paulson [Tue, 08 Jun 1999 10:25:12 +0200] rev 6799
new classical example from Lewis Carroll via S G Pulman
Mon, 07 Jun 1999 22:18:26 +0200 tuned mode_name;
changeset
wenzelm [Mon, 07 Jun 1999 22:18:26 +0200] rev 6798
tuned mode_name; improved handling of assumptions; eliminated let_thms (named prop bindings moved to auto_bind.ML);
Mon, 07 Jun 1999 22:17:23 +0200 improved handling of assumptions;
changeset
wenzelm [Mon, 07 Jun 1999 22:17:23 +0200] rev 6797
improved handling of assumptions;
Mon, 07 Jun 1999 22:16:56 +0200 facts: bind named props (from proof.ML/let_thms);
changeset
wenzelm [Mon, 07 Jun 1999 22:16:56 +0200] rev 6796
facts: bind named props (from proof.ML/let_thms);
Mon, 07 Jun 1999 21:22:18 +0200 reset HOL_quantifiers by default;
changeset
wenzelm [Mon, 07 Jun 1999 21:22:18 +0200] rev 6795
reset HOL_quantifiers by default;
Mon, 07 Jun 1999 19:25:12 +0200 Added lots of 'replicate' lemmas.
changeset
nipkow [Mon, 07 Jun 1999 19:25:12 +0200] rev 6794
Added lots of 'replicate' lemmas.
Sat, 05 Jun 1999 21:43:02 +0200 groups as monoids;
changeset
wenzelm [Sat, 05 Jun 1999 21:43:02 +0200] rev 6793
groups as monoids; tuned;
Sat, 05 Jun 1999 21:38:30 +0200 tuned comments;
changeset
wenzelm [Sat, 05 Jun 1999 21:38:30 +0200] rev 6792
tuned comments;
Sat, 05 Jun 1999 20:37:29 +0200 added Ord.order_antisym;
changeset
wenzelm [Sat, 05 Jun 1999 20:37:29 +0200] rev 6791
added Ord.order_antisym;
Sat, 05 Jun 1999 20:34:53 +0200 auto_bind_goal, auto_bind_facts;
changeset
wenzelm [Sat, 05 Jun 1999 20:34:53 +0200] rev 6790
auto_bind_goal, auto_bind_facts; varify_tfrees: no longer generalize types of free term variables; let_thms: no bindings;
Sat, 05 Jun 1999 20:33:27 +0200 auto_bind_goal, auto_bind_facts;
changeset
wenzelm [Sat, 05 Jun 1999 20:33:27 +0200] rev 6789
auto_bind_goal, auto_bind_facts;
Sat, 05 Jun 1999 20:32:49 +0200 added get_st;
changeset
wenzelm [Sat, 05 Jun 1999 20:32:49 +0200] rev 6788
added get_st;
Sat, 05 Jun 1999 20:32:10 +0200 tuned;
changeset
wenzelm [Sat, 05 Jun 1999 20:32:10 +0200] rev 6787
tuned;
Sat, 05 Jun 1999 20:30:29 +0200 varifyT': observe additional 'fixed' tfrees;
changeset
wenzelm [Sat, 05 Jun 1999 20:30:29 +0200] rev 6786
varifyT': observe additional 'fixed' tfrees;
Sat, 05 Jun 1999 20:29:07 +0200 removed ObjectLogic.setup;
changeset
wenzelm [Sat, 05 Jun 1999 20:29:07 +0200] rev 6785
removed ObjectLogic.setup;
Sat, 05 Jun 1999 20:28:45 +0200 proper calculation;
changeset
wenzelm [Sat, 05 Jun 1999 20:28:45 +0200] rev 6784
proper calculation;
Sat, 05 Jun 1999 20:27:53 +0200 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
changeset
wenzelm [Sat, 05 Jun 1999 20:27:53 +0200] rev 6783
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
Fri, 04 Jun 1999 22:12:33 +0200 fixed "...": dest_arg;
changeset
wenzelm [Fri, 04 Jun 1999 22:12:33 +0200] rev 6782
fixed "...": dest_arg;
(0) -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip
isabelle