isabelle: Changelog

instance int :: ordered_ring moved to Ring_and_Field_Example, because it changes the way that int expressions get simplified, violating the strict library principle (cf. README.html);

Sat, 20 Jan 2001 00:32:56 +0100 added Library/Ring_and_Field_Example.thy;

changeset

wenzelm [Sat, 20 Jan 2001 00:32:56 +0100] rev 10945

added Library/Ring_and_Field_Example.thy;

Sat, 20 Jan 2001 00:01:40 +0100 *** empty log message ***

changeset

wenzelm [Sat, 20 Jan 2001 00:01:40 +0100] rev 10944

*** empty log message ***

Fri, 19 Jan 2001 23:53:07 +0100 added HOL/Library/Nested_Environment.thy;

changeset

wenzelm [Fri, 19 Jan 2001 23:53:07 +0100] rev 10943

added HOL/Library/Nested_Environment.thy;

Fri, 19 Jan 2001 23:28:50 +0100 updated;

changeset

wenzelm [Fri, 19 Jan 2001 23:28:50 +0100] rev 10942

updated;

Fri, 19 Jan 2001 19:26:02 +0100 more bugs;

changeset

wenzelm [Fri, 19 Jan 2001 19:26:02 +0100] rev 10941

more bugs;

Fri, 19 Jan 2001 13:35:11 +0100 forget RPM;

changeset

wenzelm [Fri, 19 Jan 2001 13:35:11 +0100] rev 10940

forget RPM;

Fri, 19 Jan 2001 11:53:21 +0100 convert legacy tactic scripts to Isabelle/Isar tactic emulation;

changeset

wenzelm [Fri, 19 Jan 2001 11:53:21 +0100] rev 10939

convert legacy tactic scripts to Isabelle/Isar tactic emulation;

Thu, 18 Jan 2001 21:41:36 +0100 made SML/XL happy;

changeset

wenzelm [Thu, 18 Jan 2001 21:41:36 +0100] rev 10938

made SML/XL happy;

Thu, 18 Jan 2001 20:40:47 +0100 tuned;

changeset

wenzelm [Thu, 18 Jan 2001 20:40:47 +0100] rev 10937

tuned;

Thu, 18 Jan 2001 20:40:33 +0100 show(_i): check goal;

changeset

wenzelm [Thu, 18 Jan 2001 20:40:33 +0100] rev 10936

show(_i): check goal;

Thu, 18 Jan 2001 20:39:53 +0100 show/thus: check_goal;

changeset

wenzelm [Thu, 18 Jan 2001 20:39:53 +0100] rev 10935

show/thus: check_goal;

Thu, 18 Jan 2001 20:38:58 +0100 show/thus: Toplevel.proof';

changeset

wenzelm [Thu, 18 Jan 2001 20:38:58 +0100] rev 10934

show/thus: Toplevel.proof';

Thu, 18 Jan 2001 20:38:32 +0100 infix \\\\;

changeset

wenzelm [Thu, 18 Jan 2001 20:38:32 +0100] rev 10933

infix \\\\;

Thu, 18 Jan 2001 20:37:38 +0100 added exists_stamp;

changeset

wenzelm [Thu, 18 Jan 2001 20:37:38 +0100] rev 10932

added exists_stamp; added PureN, CPureN;

Thu, 18 Jan 2001 20:36:57 +0100 use Sign.PureN, Sign.CPureN;

changeset

wenzelm [Thu, 18 Jan 2001 20:36:57 +0100] rev 10931

use Sign.PureN, Sign.CPureN;

Thu, 18 Jan 2001 20:36:31 +0100 Sign.exists_stamp;

changeset

wenzelm [Thu, 18 Jan 2001 20:36:31 +0100] rev 10930

Sign.exists_stamp;

Thu, 18 Jan 2001 20:36:08 +0100 tuned \<And> and \<Or>;

changeset

wenzelm [Thu, 18 Jan 2001 20:36:08 +0100] rev 10929

tuned \<And> and \<Or>;

Thu, 18 Jan 2001 20:35:39 +0100 generate index.html for pdf docs;

changeset

wenzelm [Thu, 18 Jan 2001 20:35:39 +0100] rev 10928

generate index.html for pdf docs;

Thu, 18 Jan 2001 20:23:51 +0100 splitted Loop rule

changeset

oheimb [Thu, 18 Jan 2001 20:23:51 +0100] rev 10927

splitted Loop rule

Thu, 18 Jan 2001 18:39:43 +0100 removed redundant proof

changeset

paulson [Thu, 18 Jan 2001 18:39:43 +0100] rev 10926

removed redundant proof

Thu, 18 Jan 2001 17:38:56 +0100 is_class and class now as defs (rather than translations); corrected Digest.thy

changeset

oheimb [Thu, 18 Jan 2001 17:38:56 +0100] rev 10925

is_class and class now as defs (rather than translations); corrected Digest.thy

Tue, 16 Jan 2001 21:54:43 +0100 use_output: proper handling of non-ASCII symbols;

changeset

wenzelm [Tue, 16 Jan 2001 21:54:43 +0100] rev 10924

use_output: proper handling of non-ASCII symbols;

Tue, 16 Jan 2001 21:53:57 +0100 export plain_output;

changeset

wenzelm [Tue, 16 Jan 2001 21:53:57 +0100] rev 10923

export plain_output;

Tue, 16 Jan 2001 19:22:13 +0100 Store.thy is obsolete (newref isn't used any more)

changeset

kleing [Tue, 16 Jan 2001 19:22:13 +0100] rev 10922

Store.thy is obsolete (newref isn't used any more)

Tue, 16 Jan 2001 19:21:21 +0100 removed obsolete MicroJava/JVM/Store.thy

changeset

kleing [Tue, 16 Jan 2001 19:21:21 +0100] rev 10921

removed obsolete MicroJava/JVM/Store.thy

Tue, 16 Jan 2001 15:56:34 +0100 newref -> new_Addr

changeset

kleing [Tue, 16 Jan 2001 15:56:34 +0100] rev 10920

newref -> new_Addr

Tue, 16 Jan 2001 12:20:52 +0100 renamings: real_of_nat, real_of_int -> (overloaded) real

changeset

paulson [Tue, 16 Jan 2001 12:20:52 +0100] rev 10919

renamings: real_of_nat, real_of_int -> (overloaded) real inf_close -> approx SReal -> Reals SNat -> Nats

Tue, 16 Jan 2001 00:40:57 +0100 renamed Product_Type.split to split_conv;

changeset

wenzelm [Tue, 16 Jan 2001 00:40:57 +0100] rev 10918

renamed Product_Type.split to split_conv;

Tue, 16 Jan 2001 00:38:59 +0100 use Syntax.read_xnum;

changeset

wenzelm [Tue, 16 Jan 2001 00:38:59 +0100] rev 10917

use Syntax.read_xnum;

Tue, 16 Jan 2001 00:38:25 +0100 tuned examples;

changeset

wenzelm [Tue, 16 Jan 2001 00:38:25 +0100] rev 10916

tuned examples;

Tue, 16 Jan 2001 00:37:41 +0100 * HOL/datatype: induction rule for arbitrarily branching datatypes is

changeset

wenzelm [Tue, 16 Jan 2001 00:37:41 +0100] rev 10915

* HOL/datatype: induction rule for arbitrarily branching datatypes is now expressed as a proper nested rule (old-style tactic scripts may require atomize_strip_tac to cope with non-atomic premises); * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule to "split_conv" (old name still available for compatibility); * HOL: improved concrete syntax for strings (e.g. allows translation rules with string literals);

Tue, 16 Jan 2001 00:35:50 +0100 use_text etc.: proper output of error messages;

changeset

wenzelm [Tue, 16 Jan 2001 00:35:50 +0100] rev 10914

use_text etc.: proper output of error messages;

Tue, 16 Jan 2001 00:35:18 +0100 export fold_ast etc.;

changeset

wenzelm [Tue, 16 Jan 2001 00:35:18 +0100] rev 10913

export fold_ast etc.;

Tue, 16 Jan 2001 00:34:31 +0100 removed Session.finish ();

changeset

wenzelm [Tue, 16 Jan 2001 00:34:31 +0100] rev 10912

removed Session.finish ();