Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wed, 16 Apr 2008 17:40:59 +0200 removed unused TLA/Memory/MIParameters.thy;
changeset
wenzelm [Wed, 16 Apr 2008 17:40:59 +0200] rev 26688
removed unused TLA/Memory/MIParameters.thy;
Wed, 16 Apr 2008 17:40:43 +0200 removed obsolete valid_thms;
changeset
wenzelm [Wed, 16 Apr 2008 17:40:43 +0200] rev 26687
removed obsolete valid_thms; removed obsolete premsN binding; PureThy.get_fact: pass dynamic context;
Wed, 16 Apr 2008 17:40:42 +0200 removed obsolete premsN;
changeset
wenzelm [Wed, 16 Apr 2008 17:40:42 +0200] rev 26686
removed obsolete premsN;
Wed, 16 Apr 2008 17:40:41 +0200 PureThy.get_fact: pass dynamic context;
changeset
wenzelm [Wed, 16 Apr 2008 17:40:41 +0200] rev 26685
PureThy.get_fact: pass dynamic context;
Wed, 16 Apr 2008 17:40:40 +0200 tuned;
changeset
wenzelm [Wed, 16 Apr 2008 17:40:40 +0200] rev 26684
tuned;
Wed, 16 Apr 2008 17:40:39 +0200 removed obsolete get_fact_silent;
changeset
wenzelm [Wed, 16 Apr 2008 17:40:39 +0200] rev 26683
removed obsolete get_fact_silent; PureThy.get_fact: pass dynamic context; tuned;
Wed, 16 Apr 2008 17:40:38 +0200 tuned proofs;
changeset
wenzelm [Wed, 16 Apr 2008 17:40:38 +0200] rev 26682
tuned proofs;
Wed, 16 Apr 2008 11:24:09 +0200 Added entry for unused_thms command.
changeset
berghofe [Wed, 16 Apr 2008 11:24:09 +0200] rev 26681
Added entry for unused_thms command.
Wed, 16 Apr 2008 11:01:30 +0200 Adapted to new primrec package.
changeset
berghofe [Wed, 16 Apr 2008 11:01:30 +0200] rev 26680
Adapted to new primrec package.
Wed, 16 Apr 2008 10:57:46 +0200 Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).
changeset
berghofe [Wed, 16 Apr 2008 10:57:46 +0200] rev 26679
Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).
Wed, 16 Apr 2008 10:50:37 +0200 educated guess for infix syntax
changeset
haftmann [Wed, 16 Apr 2008 10:50:37 +0200] rev 26678
educated guess for infix syntax
Wed, 16 Apr 2008 02:25:06 +0200 removed test artefacts
changeset
urbanc [Wed, 16 Apr 2008 02:25:06 +0200] rev 26677
removed test artefacts
Tue, 15 Apr 2008 22:09:24 +0200 proof endings: no Toplevel.print!
changeset
wenzelm [Tue, 15 Apr 2008 22:09:24 +0200] rev 26676
proof endings: no Toplevel.print!
Tue, 15 Apr 2008 22:09:23 +0200 all_valid_thms: use new facts tables;
changeset
wenzelm [Tue, 15 Apr 2008 22:09:23 +0200] rev 26675
all_valid_thms: use new facts tables;
Tue, 15 Apr 2008 18:49:29 +0200 Theory.subthy;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:29 +0200] rev 26674
Theory.subthy;
Tue, 15 Apr 2008 18:49:28 +0200 Facts.intern, Facts.extern_table;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:28 +0200] rev 26673
Facts.intern, Facts.extern_table;
Tue, 15 Apr 2008 18:49:27 +0200 IsarCmd.hide_names;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:27 +0200] rev 26672
IsarCmd.hide_names;
Tue, 15 Apr 2008 18:49:26 +0200 added hide_names command (formerly Sign.hide_names), support fact name space;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:26 +0200] rev 26671
added hide_names command (formerly Sign.hide_names), support fact name space;
Tue, 15 Apr 2008 18:49:25 +0200 Facts.dest_table, PureThy.facts_of;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:25 +0200] rev 26670
Facts.dest_table, PureThy.facts_of;
Tue, 15 Apr 2008 18:49:24 +0200 simplified hide_XXX interfaces;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:24 +0200] rev 26669
simplified hide_XXX interfaces;
Tue, 15 Apr 2008 18:49:23 +0200 removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:23 +0200] rev 26668
removed obsolete SIGN_THEORY -- no name aliases in structure Theory; removed obsolete BASIC_THEORY;
Tue, 15 Apr 2008 18:49:22 +0200 removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:22 +0200] rev 26667
removed obsolete SIGN_THEORY -- no name aliases in structure Theory; simplified hide_XXX interfaces; moved hide_names to isar_cmd.ML;
Tue, 15 Apr 2008 18:49:21 +0200 added intern_fact, check_fact, hide_fact;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:21 +0200] rev 26666
added intern_fact, check_fact, hide_fact; renamed all_facts_of to facts_of; removed hide_thms; Sign.hide_const;
Tue, 15 Apr 2008 18:49:19 +0200 Theory.eq_thy;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:19 +0200] rev 26665
Theory.eq_thy;
Tue, 15 Apr 2008 18:49:18 +0200 renamed dest to dest_table, and extern to extern table;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:18 +0200] rev 26664
renamed dest to dest_table, and extern to extern table; added name space intern/extern;
Tue, 15 Apr 2008 18:49:16 +0200 PureThy.hide_fact;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:16 +0200] rev 26663
PureThy.hide_fact;
Tue, 15 Apr 2008 18:49:15 +0200 Facts.dest_table;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:15 +0200] rev 26662
Facts.dest_table;
Tue, 15 Apr 2008 18:49:13 +0200 Sign.hide_const;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:13 +0200] rev 26661
Sign.hide_const;
Tue, 15 Apr 2008 18:49:12 +0200 added hide fact;
changeset
wenzelm [Tue, 15 Apr 2008 18:49:12 +0200] rev 26660
added hide fact;
Tue, 15 Apr 2008 16:25:14 +0200 tuned;
changeset
wenzelm [Tue, 15 Apr 2008 16:25:14 +0200] rev 26659
tuned;
Tue, 15 Apr 2008 16:12:18 +0200 removed eval_antiquotes_fn;
changeset
wenzelm [Tue, 15 Apr 2008 16:12:18 +0200] rev 26658
removed eval_antiquotes_fn; eval: CRITICAL for now;
Tue, 15 Apr 2008 16:12:16 +0200 merge: canonical order;
changeset
wenzelm [Tue, 15 Apr 2008 16:12:16 +0200] rev 26657
merge: canonical order;
Tue, 15 Apr 2008 16:12:15 +0200 Library.is_equal;
changeset
wenzelm [Tue, 15 Apr 2008 16:12:15 +0200] rev 26656
Library.is_equal;
Tue, 15 Apr 2008 16:12:13 +0200 moved forall_elim_var(s) to more_thm.ML;
changeset
wenzelm [Tue, 15 Apr 2008 16:12:13 +0200] rev 26655
moved forall_elim_var(s) to more_thm.ML; get_thm(s) and hide_thms: use new table;
Tue, 15 Apr 2008 16:12:11 +0200 disallow duplicate entries (weak version for merge);
changeset
wenzelm [Tue, 15 Apr 2008 16:12:11 +0200] rev 26654
disallow duplicate entries (weak version for merge); added hide;
Tue, 15 Apr 2008 16:12:05 +0200 Thm.forall_elim_var(s);
changeset
wenzelm [Tue, 15 Apr 2008 16:12:05 +0200] rev 26653
Thm.forall_elim_var(s);
Tue, 15 Apr 2008 16:12:01 +0200 proper dynamic facts for eqvts, freshs, bijs;
changeset
wenzelm [Tue, 15 Apr 2008 16:12:01 +0200] rev 26652
proper dynamic facts for eqvts, freshs, bijs; removed obsolete print_data -- facts are accesivle via regular names; misc tuning/simplification;
Tue, 15 Apr 2008 16:11:58 +0200 overloading perm: use big_name;
changeset
wenzelm [Tue, 15 Apr 2008 16:11:58 +0200] rev 26651
overloading perm: use big_name; avoid rebinding of perm_closed -- leftover debug code;
Tue, 15 Apr 2008 16:11:52 +0200 * Name space merge now observes canonical order;
changeset
wenzelm [Tue, 15 Apr 2008 16:11:52 +0200] rev 26650
* Name space merge now observes canonical order; * Authentic naming of facts;
Mon, 14 Apr 2008 22:29:56 +0200 removed redundant hd_append variant;
changeset
wenzelm [Mon, 14 Apr 2008 22:29:56 +0200] rev 26649
removed redundant hd_append variant;
Mon, 14 Apr 2008 21:44:53 +0200 removed duplicate lemmas;
changeset
wenzelm [Mon, 14 Apr 2008 21:44:53 +0200] rev 26648
removed duplicate lemmas;
Mon, 14 Apr 2008 21:44:53 +0200 avoid duplicate fact bindings;
changeset
wenzelm [Mon, 14 Apr 2008 21:44:53 +0200] rev 26647
avoid duplicate fact bindings;
Mon, 14 Apr 2008 21:44:51 +0200 overloading of perm: adhoc name prevents duplicate fact names;
changeset
wenzelm [Mon, 14 Apr 2008 21:44:51 +0200] rev 26646
overloading of perm: adhoc name prevents duplicate fact names;
Mon, 14 Apr 2008 17:54:56 +0200 Changed naming scheme for theorems generated by interpretations.
changeset
ballarin [Mon, 14 Apr 2008 17:54:56 +0200] rev 26645
Changed naming scheme for theorems generated by interpretations.
Mon, 14 Apr 2008 16:42:47 +0200 proper context for induct_scheme method
changeset
krauss [Mon, 14 Apr 2008 16:42:47 +0200] rev 26644
proper context for induct_scheme method
Mon, 14 Apr 2008 14:28:47 +0200 Isar.toplevel_loop: separate init/welcome flag;
changeset
wenzelm [Mon, 14 Apr 2008 14:28:47 +0200] rev 26643
Isar.toplevel_loop: separate init/welcome flag;
Sun, 13 Apr 2008 16:40:08 +0200 Sorts.class_error: produce message only (formerly msg_class_error);
changeset
wenzelm [Sun, 13 Apr 2008 16:40:08 +0200] rev 26642
Sorts.class_error: produce message only (formerly msg_class_error);
Sun, 13 Apr 2008 16:40:07 +0200 tsig: removed unnecessary universal witness;
changeset
wenzelm [Sun, 13 Apr 2008 16:40:07 +0200] rev 26641
tsig: removed unnecessary universal witness; Sorts.class_error: produce message only (formerly msg_class_error);
Sun, 13 Apr 2008 16:40:06 +0200 simplified handling of sorts, removed unnecessary universal witness;
changeset
wenzelm [Sun, 13 Apr 2008 16:40:06 +0200] rev 26640
simplified handling of sorts, removed unnecessary universal witness; Envir.insert_sorts;
Sun, 13 Apr 2008 16:40:05 +0200 removed unused minimal_classes;
changeset
wenzelm [Sun, 13 Apr 2008 16:40:05 +0200] rev 26639
removed unused minimal_classes; class_error: produce message only (formerly msg_class_error); tuned;
Sun, 13 Apr 2008 16:40:04 +0200 added insert_sorts (from thm.ML);
changeset
wenzelm [Sun, 13 Apr 2008 16:40:04 +0200] rev 26638
added insert_sorts (from thm.ML);
Sun, 13 Apr 2008 16:40:02 +0200 tsig: removed unnecessary universal witness;
changeset
wenzelm [Sun, 13 Apr 2008 16:40:02 +0200] rev 26637
tsig: removed unnecessary universal witness;
Sun, 13 Apr 2008 14:30:23 +0200 tuned;
changeset
wenzelm [Sun, 13 Apr 2008 14:30:23 +0200] rev 26636
tuned;
Sat, 12 Apr 2008 17:00:50 +0200 removed unnecessary Goal.close_result;
changeset
wenzelm [Sat, 12 Apr 2008 17:00:50 +0200] rev 26635
removed unnecessary Goal.close_result;
Sat, 12 Apr 2008 17:00:48 +0200 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
changeset
wenzelm [Sat, 12 Apr 2008 17:00:48 +0200] rev 26634
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression); pred_def: tag internal;
Sat, 12 Apr 2008 17:00:47 +0200 advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
changeset
wenzelm [Sat, 12 Apr 2008 17:00:47 +0200] rev 26633
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
Sat, 12 Apr 2008 17:00:47 +0200 added is_utf8_trailer;
changeset
wenzelm [Sat, 12 Apr 2008 17:00:47 +0200] rev 26632
added is_utf8_trailer;
Sat, 12 Apr 2008 17:00:45 +0200 rep_cterm/rep_thm: no longer dereference theory_ref;
changeset
wenzelm [Sat, 12 Apr 2008 17:00:45 +0200] rev 26631
rep_cterm/rep_thm: no longer dereference theory_ref; removed obsolete compression;
Sat, 12 Apr 2008 17:00:43 +0200 obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;
changeset
wenzelm [Sat, 12 Apr 2008 17:00:43 +0200] rev 26630
obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;
Sat, 12 Apr 2008 17:00:42 +0200 removed obsolete compress.ML
changeset
wenzelm [Sat, 12 Apr 2008 17:00:42 +0200] rev 26629
removed obsolete compress.ML
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle