isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

Fri, 01 May 1998 11:43:38 +0200 *** empty log message ***

nipkow [Fri, 01 May 1998 11:43:38 +0200] rev 4880

*** empty log message ***

Fri, 01 May 1998 11:23:04 +0200 "let" is no longer restricted to FOL terms and allows any logical terms

paulson [Fri, 01 May 1998 11:23:04 +0200] rev 4879

"let" is no longer restricted to FOL terms and allows any logical terms

Fri, 01 May 1998 11:22:09 +0200 Let.ML and Let.thy had been omitted

paulson [Fri, 01 May 1998 11:22:09 +0200] rev 4878

Let.ML and Let.thy had been omitted

Thu, 30 Apr 1998 17:16:25 +0200 fixed simpset(), claset();

wenzelm [Thu, 30 Apr 1998 17:16:25 +0200] rev 4877

fixed simpset(), claset();

Wed, 29 Apr 1998 11:46:42 +0200 moved records data to Tools/record_package.ML;

wenzelm [Wed, 29 Apr 1998 11:46:42 +0200] rev 4876

moved records data to Tools/record_package.ML; tuned setup;

Wed, 29 Apr 1998 11:45:41 +0200 nontermials;

wenzelm [Wed, 29 Apr 1998 11:45:41 +0200] rev 4875

nontermials;

Wed, 29 Apr 1998 11:45:16 +0200 Theory.require;

wenzelm [Wed, 29 Apr 1998 11:45:16 +0200] rev 4874

Theory.require; adapted to new PureThy.add_defs_i, PureThy.add_axioms;

Wed, 29 Apr 1998 11:44:30 +0200 TypedefPackage.add_typedef;

wenzelm [Wed, 29 Apr 1998 11:44:30 +0200] rev 4873

TypedefPackage.add_typedef; RecordPackage.add_record;

Wed, 29 Apr 1998 11:43:53 +0200 Theory.require;

wenzelm [Wed, 29 Apr 1998 11:43:53 +0200] rev 4872

Theory.require;

Wed, 29 Apr 1998 11:43:34 +0200 Logic.mk_defpair;

wenzelm [Wed, 29 Apr 1998 11:43:34 +0200] rev 4871

Logic.mk_defpair; adapted to new PureThy.add_defs_i;

Wed, 29 Apr 1998 11:42:04 +0200 Extensible records with structural subtyping in HOL. See

wenzelm [Wed, 29 Apr 1998 11:42:04 +0200] rev 4870

Extensible records with structural subtyping in HOL. See Tools/record_package.ML for the actual implementation.

Wed, 29 Apr 1998 11:41:36 +0200 new theory section 'setup';

wenzelm [Wed, 29 Apr 1998 11:41:36 +0200] rev 4869

new theory section 'setup';

Wed, 29 Apr 1998 11:41:08 +0200 nonterminals;

wenzelm [Wed, 29 Apr 1998 11:41:08 +0200] rev 4868

nonterminals; tuned setup;

Wed, 29 Apr 1998 11:40:37 +0200 package extensible records with structural subtyping in HOL -- still

wenzelm [Wed, 29 Apr 1998 11:40:37 +0200] rev 4867

package extensible records with structural subtyping in HOL -- still experimental version;

Wed, 29 Apr 1998 11:39:52 +0200 renamed from typedef.ML;

wenzelm [Wed, 29 Apr 1998 11:39:52 +0200] rev 4866

renamed from typedef.ML;

Wed, 29 Apr 1998 11:39:28 +0200 reworked and moved to Tools/record_package.ML;

wenzelm [Wed, 29 Apr 1998 11:39:28 +0200] rev 4865

reworked and moved to Tools/record_package.ML;

Wed, 29 Apr 1998 11:38:52 +0200 removed typedef.ML, record.ML;

wenzelm [Wed, 29 Apr 1998 11:38:52 +0200] rev 4864

removed typedef.ML, record.ML; added Tools/typedef_package.ML, Tools/record_package.ML, Record.thy;

Wed, 29 Apr 1998 11:37:58 +0200 renamed to Tools/typedef_package.ML;

wenzelm [Wed, 29 Apr 1998 11:37:58 +0200] rev 4863

renamed to Tools/typedef_package.ML;

Wed, 29 Apr 1998 11:36:53 +0200 adapted to new PureThy.add_axioms_i;

wenzelm [Wed, 29 Apr 1998 11:36:53 +0200] rev 4862

adapted to new PureThy.add_axioms_i; Theory.parent_path;

Wed, 29 Apr 1998 11:36:08 +0200 adapted to new PureThy.add_tthmss;

wenzelm [Wed, 29 Apr 1998 11:36:08 +0200] rev 4861

adapted to new PureThy.add_tthmss; Theory.parent_path;

Wed, 29 Apr 1998 11:35:24 +0200 Theory.require;

wenzelm [Wed, 29 Apr 1998 11:35:24 +0200] rev 4860

Theory.require; Logic.mk_defpair; adapted to new PureThy.add_defs_i;

Wed, 29 Apr 1998 11:34:11 +0200 adapted to new PureThy.add_axioms;

wenzelm [Wed, 29 Apr 1998 11:34:11 +0200] rev 4859

adapted to new PureThy.add_axioms;

Wed, 29 Apr 1998 11:33:44 +0200 new theory section 'nonterminals';

wenzelm [Wed, 29 Apr 1998 11:33:44 +0200] rev 4858

new theory section 'nonterminals';

Wed, 29 Apr 1998 11:33:27 +0200 adapted to new PureThy.add_defs;

wenzelm [Wed, 29 Apr 1998 11:33:27 +0200] rev 4857

adapted to new PureThy.add_defs;

Wed, 29 Apr 1998 11:33:06 +0200 Theory.require;

wenzelm [Wed, 29 Apr 1998 11:33:06 +0200] rev 4856

Theory.require;

Wed, 29 Apr 1998 11:30:55 +0200 tuned setup;

wenzelm [Wed, 29 Apr 1998 11:30:55 +0200] rev 4855

tuned setup; simp_add_global, simp_del_global, simp_add_local, simp_del_local attributes;

Wed, 29 Apr 1998 11:29:39 +0200 tuned setup;

wenzelm [Wed, 29 Apr 1998 11:29:39 +0200] rev 4854

tuned setup;

Wed, 29 Apr 1998 11:29:00 +0200 tuned names of (add_)store_XXX functions;

wenzelm [Wed, 29 Apr 1998 11:29:00 +0200] rev 4853

tuned names of (add_)store_XXX functions; added attributes to add_thms, add_axioms, add_defs functions;

Wed, 29 Apr 1998 11:26:59 +0200 replaced thy_setup by 'setup' section;

wenzelm [Wed, 29 Apr 1998 11:26:59 +0200] rev 4852

replaced thy_setup by 'setup' section; adapted to new PureThy.add_axioms / PureThy.add_defs; added 'nonterminals' section;

Wed, 29 Apr 1998 11:25:26 +0200 added append;

wenzelm [Wed, 29 Apr 1998 11:25:26 +0200] rev 4851

added append;

Wed, 29 Apr 1998 11:24:58 +0200 added none: 'a -> 'a * 'b attribute list;

wenzelm [Wed, 29 Apr 1998 11:24:58 +0200] rev 4850

added none: 'a -> 'a * 'b attribute list; added no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list; added no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list; added applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list);

Wed, 29 Apr 1998 11:22:52 +0200 tuned error msgs;

wenzelm [Wed, 29 Apr 1998 11:22:52 +0200] rev 4849

tuned error msgs;

Wed, 29 Apr 1998 11:22:01 +0200 moved mk_defpair to logic.ML;

wenzelm [Wed, 29 Apr 1998 11:22:01 +0200] rev 4848

moved mk_defpair to logic.ML; moved get_def to thm.ML; moved require_thy to theory.ML;

Wed, 29 Apr 1998 11:20:53 +0200 tuned get_ax (uses ancestry);

wenzelm [Wed, 29 Apr 1998 11:20:53 +0200] rev 4847

tuned get_ax (uses ancestry); added get_def: theory -> xstring -> thm;

Wed, 29 Apr 1998 11:17:14 +0200 renamed setup to apply;

wenzelm [Wed, 29 Apr 1998 11:17:14 +0200] rev 4846

renamed setup to apply; added add_nonterminals: bstring list -> theory -> theory; added parent_path: theory -> theory; added root_path: theory -> theory; added require: theory -> string -> string -> unit (from section_utils.ML);

Wed, 29 Apr 1998 11:14:34 +0200 adapted to new PureThy.add_axioms_i;

wenzelm [Wed, 29 Apr 1998 11:14:34 +0200] rev 4845

adapted to new PureThy.add_axioms_i;

Wed, 29 Apr 1998 11:13:22 +0200 added defaultS: sg -> sort;

wenzelm [Wed, 29 Apr 1998 11:13:22 +0200] rev 4844

added defaultS: sg -> sort; added full_name_path: sg -> string -> bstring -> string; added add_nonterminals: bstring list -> sg -> sg;

Wed, 29 Apr 1998 11:11:36 +0200 added thm, thms;

wenzelm [Wed, 29 Apr 1998 11:11:36 +0200] rev 4843

added thm, thms;

Wed, 29 Apr 1998 11:10:40 +0200 *** empty log message ***

wenzelm [Wed, 29 Apr 1998 11:10:40 +0200] rev 4842

*** empty log message ***

Tue, 28 Apr 1998 13:52:18 +0200 new thms, really demos of the final coalgebra theorem

paulson [Tue, 28 Apr 1998 13:52:18 +0200] rev 4841

new thms, really demos of the final coalgebra theorem

Tue, 28 Apr 1998 13:51:39 +0200 new thms image_0_left, image_Un_left, etc.

paulson [Tue, 28 Apr 1998 13:51:39 +0200] rev 4840

new thms image_0_left, image_Un_left, etc.

Tue, 28 Apr 1998 13:50:41 +0200 new thm mult_lt_mono1

paulson [Tue, 28 Apr 1998 13:50:41 +0200] rev 4839

new thm mult_lt_mono1

Mon, 27 Apr 1998 19:32:19 +0200 cleanup for split_all_tac as wrapper in claset()

oheimb [Mon, 27 Apr 1998 19:32:19 +0200] rev 4838

cleanup for split_all_tac as wrapper in claset()

Mon, 27 Apr 1998 19:30:40 +0200 removed wrong comment

oheimb [Mon, 27 Apr 1998 19:30:40 +0200] rev 4837

removed wrong comment

Mon, 27 Apr 1998 19:29:19 +0200 added option_map_eq_Some via AddIffs

oheimb [Mon, 27 Apr 1998 19:29:19 +0200] rev 4836

added option_map_eq_Some via AddIffs

Mon, 27 Apr 1998 18:06:22 +0200 *** empty log message ***

nipkow [Mon, 27 Apr 1998 18:06:22 +0200] rev 4835

*** empty log message ***

Mon, 27 Apr 1998 17:52:03 +0200 delsplits, Addsplits, Delsplits.

nipkow [Mon, 27 Apr 1998 17:52:03 +0200] rev 4834

delsplits, Addsplits, Delsplits.

Mon, 27 Apr 1998 16:47:50 +0200 Renamed expand_const -> split_const

nipkow [Mon, 27 Apr 1998 16:47:50 +0200] rev 4833

Renamed expand_const -> split_const

Mon, 27 Apr 1998 16:46:56 +0200 Added conversion of reg.expr. to automata.

nipkow [Mon, 27 Apr 1998 16:46:56 +0200] rev 4832

Added conversion of reg.expr. to automata. Renamed expand_const -> split_const.

Mon, 27 Apr 1998 16:45:27 +0200 Renamed expand_const -> split_const.

nipkow [Mon, 27 Apr 1998 16:45:27 +0200] rev 4831

Renamed expand_const -> split_const.

Mon, 27 Apr 1998 16:45:11 +0200 Added a few lemmas.

nipkow [Mon, 27 Apr 1998 16:45:11 +0200] rev 4830

Added a few lemmas. Renamed expand_const -> split_const.

Mon, 27 Apr 1998 13:47:46 +0200 New proof of apply_equality and new thm Pi_image_cons

paulson [Mon, 27 Apr 1998 13:47:46 +0200] rev 4829

New proof of apply_equality and new thm Pi_image_cons

Fri, 24 Apr 1998 16:18:39 +0200 improved split_all_tac significantly

oheimb [Fri, 24 Apr 1998 16:18:39 +0200] rev 4828

improved split_all_tac significantly

Fri, 24 Apr 1998 16:16:29 +0200 improved keyboard modifiers

oheimb [Fri, 24 Apr 1998 16:16:29 +0200] rev 4827

improved keyboard modifiers

Fri, 24 Apr 1998 16:15:34 +0200 added ASCII translation of subseteq

oheimb [Fri, 24 Apr 1998 16:15:34 +0200] rev 4826

added ASCII translation of subseteq

Fri, 24 Apr 1998 13:06:17 +0200 tidied; div & mod

paulson [Fri, 24 Apr 1998 13:06:17 +0200] rev 4825

tidied; div & mod

Fri, 24 Apr 1998 11:22:39 +0200 *** empty log message ***

oheimb [Fri, 24 Apr 1998 11:22:39 +0200] rev 4824

*** empty log message ***

Wed, 22 Apr 1998 19:09:44 +0200 added no_syn;

wenzelm [Wed, 22 Apr 1998 19:09:44 +0200] rev 4823

added no_syn;

Wed, 22 Apr 1998 19:08:49 +0200 added mk_cond_defpair, mk_defpair;

wenzelm [Wed, 22 Apr 1998 19:08:49 +0200] rev 4822

added mk_cond_defpair, mk_defpair;

Wed, 22 Apr 1998 14:06:05 +0200 Modifications due to improved simplifier.

nipkow [Wed, 22 Apr 1998 14:06:05 +0200] rev 4821

Modifications due to improved simplifier.

(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle