| Fri, 10 Jul 1998 15:19:10 +0200 | wenzelm | added xpm icons; | changeset | files |
| Mon, 06 Jul 1998 14:03:25 +0200 | nipkow | Converted to Auto_tac | changeset | files |
| Fri, 03 Jul 1998 18:56:40 +0200 | wenzelm | several new basic modules made available for general use; | changeset | files |
| Fri, 03 Jul 1998 18:53:02 +0200 | wenzelm | cleaned up; | changeset | files |
| Fri, 03 Jul 1998 18:05:03 +0200 | wenzelm | theory Main includes everything; | changeset | files |
| Fri, 03 Jul 1998 17:36:45 +0200 | wenzelm | reorganized the main HOL image; | changeset | files |
| Fri, 03 Jul 1998 17:35:39 +0200 | wenzelm | stepping stones: Recdef, Main; | changeset | files |
| Fri, 03 Jul 1998 17:34:55 +0200 | wenzelm | stepping stones; | changeset | files |
| Fri, 03 Jul 1998 17:34:24 +0200 | wenzelm | removed duplicate thms; | changeset | files |
| Fri, 03 Jul 1998 17:33:47 +0200 | wenzelm | moved String theory to main HOL; | changeset | files |
| Fri, 03 Jul 1998 11:02:01 +0200 | berghofe | Removed disjE from list of rules used to simplify elimination | changeset | files |
| Fri, 03 Jul 1998 10:55:32 +0200 | nipkow | Removed leading !! in goals | changeset | files |
| Fri, 03 Jul 1998 10:37:04 +0200 | nipkow | Removed leading !! in goals. | changeset | files |
| Fri, 03 Jul 1998 10:36:47 +0200 | nipkow | Removed leading !! in goals. | changeset | files |
| Thu, 02 Jul 1998 17:58:12 +0200 | paulson | Renamed expand_if to split_if and setloop split_tac to addsplits, | changeset | files |
| Thu, 02 Jul 1998 17:56:06 +0200 | paulson | HACKED declaration of addsplits | changeset | files |
| Thu, 02 Jul 1998 17:48:11 +0200 | paulson | Deleted leading parameters thanks to new Goal command | changeset | files |
| Thu, 02 Jul 1998 17:27:35 +0200 | wenzelm | tuned comment; | changeset | files |
| Thu, 02 Jul 1998 17:26:47 +0200 | wenzelm | Symbol.beginning; | changeset | files |
| Thu, 02 Jul 1998 16:53:55 +0200 | paulson | Uncurried functions LeadsTo and reach | changeset | files |
| Thu, 02 Jul 1998 16:44:39 +0200 | wenzelm | fixed Integ; | changeset | files |
| Wed, 01 Jul 1998 19:11:20 +0200 | berghofe | Adapted to new inductive definition package. | changeset | files |
| Wed, 01 Jul 1998 19:03:54 +0200 | berghofe | Fixed bug (improper handling of flag no_ind). | changeset | files |
| Wed, 01 Jul 1998 18:43:40 +0200 | berghofe | Replaced "use_dir" command by "use", because nested calls | changeset | files |
| Wed, 01 Jul 1998 17:59:25 +0200 | paulson | HOL-Real | changeset | files |
| Wed, 01 Jul 1998 11:33:39 +0200 | wenzelm | tuned Inductive.thy; | changeset | files |
| Wed, 01 Jul 1998 11:20:32 +0200 | wenzelm | added add_typedecls; | changeset | files |
| Tue, 30 Jun 1998 20:57:46 +0200 | berghofe | Removed structure Prod_Syntax. | changeset | files |
| Tue, 30 Jun 1998 20:51:15 +0200 | berghofe | Adapted to new inductive definition package. | changeset | files |
| Tue, 30 Jun 1998 20:50:34 +0200 | berghofe | Adapted to new inductive package. | changeset | files |
| Tue, 30 Jun 1998 20:49:49 +0200 | berghofe | Removed obsolete comments. | changeset | files |
| Tue, 30 Jun 1998 20:46:35 +0200 | berghofe | Removed old inductive definition package. | changeset | files |
| Tue, 30 Jun 1998 20:43:36 +0200 | berghofe | Removed structure Prod_Syntax. | changeset | files |
| Tue, 30 Jun 1998 20:42:47 +0200 | berghofe | Adapted to new inductive definition package. | changeset | files |
| Tue, 30 Jun 1998 20:41:41 +0200 | berghofe | Moved most of the Prod_Syntax - stuff to HOLogic. | changeset | files |
| Tue, 30 Jun 1998 20:40:29 +0200 | berghofe | Added additional theorems needed for inductive definitions. | changeset | files |
| Tue, 30 Jun 1998 20:39:43 +0200 | berghofe | New inductive definition package | changeset | files |
| Tue, 30 Jun 1998 14:41:27 +0200 | wenzelm | added quick_and_dirty flag; | changeset | files |
| Mon, 29 Jun 1998 21:33:35 +0200 | wenzelm | moved actual (C)Pure theories to pure.ML; | changeset | files |
| Mon, 29 Jun 1998 21:33:25 +0200 | wenzelm | tuned transaction; | changeset | files |
| Mon, 29 Jun 1998 10:32:06 +0200 | wenzelm | use_text: verbose flag; | changeset | files |
| Fri, 26 Jun 1998 15:16:14 +0200 | paulson | New rewrite unit_abs_eta_conv to compensate for unit_eq_proc | changeset | files |
| Fri, 26 Jun 1998 15:10:40 +0200 | paulson | New rewrite unit_abs_eta_conv to compensate for unit_eq_proc | changeset | files |
| Thu, 25 Jun 1998 16:28:41 +0200 | wenzelm | fixed unit_eq; | changeset | files |
| Thu, 25 Jun 1998 16:13:20 +0200 | wenzelm | delsimprocs [unit_eq_proc]; | changeset | files |
| Thu, 25 Jun 1998 16:12:02 +0200 | wenzelm | simplification procedure unit_eq_proc rewrites (?x::unit) = (); | changeset | files |
| Thu, 25 Jun 1998 15:37:36 +0200 | wenzelm | tuned loose bound vars check; | changeset | files |
| Thu, 25 Jun 1998 15:34:17 +0200 | wenzelm | added unit_eq simplification procedure; | changeset | files |
| Thu, 25 Jun 1998 15:33:30 +0200 | wenzelm | added XX_YY_rewrite: simpset -> cterm -> thm; | changeset | files |
| Thu, 25 Jun 1998 15:32:41 +0200 | wenzelm | Thm.rewrite_cterm; | changeset | files |
| Thu, 25 Jun 1998 15:22:05 +0200 | wenzelm | defaults for free variables hide consts of same name; | changeset | files |
| Thu, 25 Jun 1998 15:20:59 +0200 | wenzelm | added rewrite_cterm; | changeset | files |
| Thu, 25 Jun 1998 13:57:34 +0200 | paulson | Installation of target HOL-Real | changeset | files |
| Wed, 24 Jun 1998 13:59:45 +0200 | nipkow | * HOL/List: new function list_update written xs[i:=v] that updates the i-th | changeset | files |
| Wed, 24 Jun 1998 11:24:52 +0200 | paulson | Ran isatool fixgoal | changeset | files |
| Wed, 24 Jun 1998 10:33:42 +0200 | paulson | removed duplicate entry for Goal | changeset | files |
| Wed, 24 Jun 1998 10:30:29 +0200 | paulson | Trivial change to be more like paper | changeset | files |
| Wed, 24 Jun 1998 10:29:46 +0200 | paulson | Tidying; renaming of Says_Server_message_form to | changeset | files |
| Tue, 23 Jun 1998 18:09:16 +0200 | nipkow | *** empty log message *** | changeset | files |
| Tue, 23 Jun 1998 18:07:45 +0200 | nipkow | Consequences of the change from [ := ] to ( := ) in theory Update. | changeset | files |
| Tue, 23 Jun 1998 18:06:50 +0200 | nipkow | Replaced [ := ] syntax by ( := ). | changeset | files |
| Mon, 22 Jun 1998 17:26:46 +0200 | wenzelm | isatool fixgoal; | changeset | files |
| Mon, 22 Jun 1998 17:13:09 +0200 | wenzelm | isatool fixgoal; | changeset | files |
| Mon, 22 Jun 1998 17:12:27 +0200 | wenzelm | isatool fixgoal; | changeset | files |
| Mon, 22 Jun 1998 15:53:24 +0200 | paulson | Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb. | changeset | files |
| Mon, 22 Jun 1998 15:50:59 +0200 | paulson | comments and minor tidying | changeset | files |
| Mon, 22 Jun 1998 15:49:29 +0200 | paulson | simplified and tidied the proofs | changeset | files |
| Mon, 22 Jun 1998 15:25:06 +0200 | wenzelm | check_mlhome_file; | changeset | files |
| Mon, 22 Jun 1998 15:18:02 +0200 | wenzelm | isatool fixgoal; | changeset | files |
| Mon, 22 Jun 1998 15:09:59 +0200 | wenzelm | isatool fixgoal; | changeset | files |
| Sat, 20 Jun 1998 20:35:38 +0200 | wenzelm | def_sort; | changeset | files |
| Sat, 20 Jun 1998 20:18:51 +0200 | wenzelm | renamed Thm(s) back to thm(s); | changeset | files |
| Sat, 20 Jun 1998 20:18:22 +0200 | wenzelm | export mk_triple1/2; | changeset | files |
| Sat, 20 Jun 1998 19:53:05 +0200 | wenzelm | added read_def_axm; | changeset | files |
| Sat, 20 Jun 1998 19:52:53 +0200 | wenzelm | added fix_mixfix; | changeset | files |
| Fri, 19 Jun 1998 11:20:36 +0200 | paulson | fixed comment | changeset | files |
| Fri, 19 Jun 1998 11:14:20 +0200 | paulson | tidying | changeset | files |
| Fri, 19 Jun 1998 10:34:33 +0200 | paulson | New example Kerberos_BAN by G Bella | changeset | files |
| Thu, 18 Jun 1998 18:35:07 +0200 | wenzelm | fixed comment; | changeset | files |
| Thu, 18 Jun 1998 18:31:06 +0200 | wenzelm | tuned \s pattern; | changeset | files |
| Thu, 18 Jun 1998 18:28:45 +0200 | wenzelm | isatool fixgoal; | changeset | files |
| Thu, 18 Jun 1998 11:22:45 +0200 | wenzelm | removed Thy; | changeset | files |
| Thu, 18 Jun 1998 11:20:54 +0200 | wenzelm | replaced warning by error_msg; | changeset | files |
| Thu, 18 Jun 1998 10:52:34 +0200 | wenzelm | new toplevel commands `Goal' and `Goalw'; | changeset | files |
| Thu, 18 Jun 1998 10:50:16 +0200 | wenzelm | renamed thm(s) to Thm(s); | changeset | files |
| Thu, 18 Jun 1998 10:48:21 +0200 | wenzelm | replace goal(w) commands by implicit versions Goal(w); | changeset | files |
| Wed, 17 Jun 1998 12:44:02 +0200 | nipkow | Goal and Goalw | changeset | files |
| Wed, 17 Jun 1998 10:49:45 +0200 | nipkow | goal -> Goal | changeset | files |
| Wed, 17 Jun 1998 10:49:24 +0200 | nipkow | Changed and changed back. | changeset | files |
| Wed, 17 Jun 1998 10:48:38 +0200 | nipkow | Goals may now contain assumptions, which are not returned. | changeset | files |
| Tue, 16 Jun 1998 18:37:34 +0200 | wenzelm | added General/history.ML; | changeset | files |
| Tue, 16 Jun 1998 18:37:11 +0200 | wenzelm | Histories of values, with undo and redo; | changeset | files |
| Mon, 15 Jun 1998 11:06:00 +0200 | wenzelm | use_text replaces use_strings; | changeset | files |
| Mon, 15 Jun 1998 11:05:25 +0200 | wenzelm | handle_error: capture error msgs, even if no exception raised; | changeset | files |
| Sat, 13 Jun 1998 18:25:39 +0200 | wenzelm | removed use_text; | changeset | files |
| Fri, 12 Jun 1998 18:08:41 +0200 | wenzelm | added use_text; | changeset | files |
| Fri, 12 Jun 1998 17:07:33 +0200 | wenzelm | Context.add_session; | changeset | files |
| Fri, 12 Jun 1998 17:06:58 +0200 | wenzelm | changed (| |) syntax to (: :); | changeset | files |
| Fri, 12 Jun 1998 17:06:14 +0200 | wenzelm | changed {: :} syntax to (| |); | changeset | files |
| Fri, 12 Jun 1998 17:05:04 +0200 | wenzelm | tuned exports; | changeset | files |
| Thu, 11 Jun 1998 18:18:37 +0200 | nipkow | removed rel.ML | changeset | files |
| Thu, 11 Jun 1998 18:17:40 +0200 | nipkow | ancient relic | changeset | files |
| Wed, 10 Jun 1998 18:07:07 +0200 | wenzelm | Context.the_context; | changeset | files |
| Wed, 10 Jun 1998 17:56:57 +0200 | wenzelm | get_context renamed to the_context; | changeset | files |
| Wed, 10 Jun 1998 17:56:21 +0200 | wenzelm | tuned transaction; | changeset | files |
| Wed, 10 Jun 1998 12:13:52 +0200 | wenzelm | tuned comments; | changeset | files |
| Wed, 10 Jun 1998 12:00:51 +0200 | wenzelm | adapted to TheoryDataFun interface; | changeset | files |
| Wed, 10 Jun 1998 11:58:11 +0200 | wenzelm | moved attributes theory data to Isar/isar_thy.ML; | changeset | files |
| Wed, 10 Jun 1998 11:57:40 +0200 | wenzelm | moved add_axioms_x, add_defs_x to Isar/isar_thy.ML; | changeset | files |
| Wed, 10 Jun 1998 11:57:01 +0200 | wenzelm | added exnMessage; | changeset | files |
| Wed, 10 Jun 1998 11:56:23 +0200 | wenzelm | added General; | changeset | files |
| Wed, 10 Jun 1998 11:55:49 +0200 | wenzelm | added of_file; | changeset | files |
| Wed, 10 Jun 1998 11:55:30 +0200 | wenzelm | General tools. | changeset | files |
| Wed, 10 Jun 1998 11:55:09 +0200 | wenzelm | moved table.ML, object.ML, seq.ML, name_space.ML to General; | changeset | files |
| Wed, 10 Jun 1998 11:54:04 +0200 | wenzelm | moved object.ML to General/object.ML; | changeset | files |
| Wed, 10 Jun 1998 11:53:37 +0200 | wenzelm | moved table.ML to General/table.ML; | changeset | files |
| Wed, 10 Jun 1998 11:52:59 +0200 | wenzelm | moved seq.ML to General/seq.ML; | changeset | files |
| Wed, 10 Jun 1998 11:52:34 +0200 | wenzelm | moved position.ML, path.ML, file.ML to General; | changeset | files |
| Wed, 10 Jun 1998 11:51:58 +0200 | wenzelm | moved name_space.ML to General/name_space.ML; | changeset | files |
| Wed, 10 Jun 1998 11:51:28 +0200 | wenzelm | moved Thy/path.ML to General/path.ML; | changeset | files |
| Wed, 10 Jun 1998 11:50:52 +0200 | wenzelm | moved Thy/position.ML to General/position.ML; | changeset | files |
| Wed, 10 Jun 1998 11:50:20 +0200 | wenzelm | moved Thy/file.ML to General/file.ML; | changeset | files |
| Wed, 10 Jun 1998 11:49:41 +0200 | wenzelm | new type-safe user interface for theory data; | changeset | files |
| Tue, 09 Jun 1998 13:49:43 +0200 | wenzelm | nonterminals prog; | changeset | files |
| Tue, 09 Jun 1998 11:37:52 +0200 | wenzelm | adapted to new theory data interface; | changeset | files |
| Mon, 08 Jun 1998 15:58:56 +0200 | wenzelm | use type-safe theory data interface; | changeset | files |
| Mon, 08 Jun 1998 15:57:50 +0200 | wenzelm | added theory_data.ML; | changeset | files |
| Mon, 08 Jun 1998 15:57:30 +0200 | wenzelm | Type-safe interface for theory data. | changeset | files |
| Fri, 05 Jun 1998 14:40:07 +0200 | wenzelm | * improved the theory data mechanism to support real encapsulation; | changeset | files |
| Fri, 05 Jun 1998 14:33:18 +0200 | wenzelm | accomodate tuned version of theory data; | changeset | files |
| Fri, 05 Jun 1998 14:32:23 +0200 | wenzelm | added print_theorems: theory -> unit; | changeset | files |
| Fri, 05 Jun 1998 14:29:54 +0200 | wenzelm | Object.T; | changeset | files |
| Fri, 05 Jun 1998 14:29:33 +0200 | wenzelm | improved data: secure version using Object.T and Object.kind; | changeset | files |
| Fri, 05 Jun 1998 14:28:08 +0200 | wenzelm | tuned setup; | changeset | files |
| Fri, 05 Jun 1998 14:26:55 +0200 | wenzelm | use Object.T and Object.kind; | changeset | files |
| Fri, 05 Jun 1998 14:23:52 +0200 | wenzelm | removed type object (see object.ML); | changeset | files |
| Fri, 05 Jun 1998 14:23:27 +0200 | wenzelm | tuned print_exn; | changeset | files |
| Fri, 05 Jun 1998 14:23:07 +0200 | wenzelm | print_data moved to theory.ML; | changeset | files |
| Fri, 05 Jun 1998 14:22:11 +0200 | wenzelm | added THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq; | changeset | files |
| Fri, 05 Jun 1998 14:21:11 +0200 | wenzelm | added object.ML; | changeset | files |
| Tue, 02 Jun 1998 15:08:42 +0200 | oheimb | added option_map_o_empty | changeset | files |
| Tue, 02 Jun 1998 15:07:25 +0200 | oheimb | added split_etas | changeset | files |
| Tue, 02 Jun 1998 15:07:00 +0200 | oheimb | added split_sum_case_asm | changeset | files |
| Fri, 29 May 1998 13:50:21 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 29 May 1998 13:49:50 +0200 | wenzelm | tuned msgs; | changeset | files |
| Thu, 28 May 1998 17:21:52 +0200 | paulson | auto update | changeset | files |
| Thu, 28 May 1998 17:02:29 +0200 | wenzelm | fixed ml_prompts; | changeset | files |
| Thu, 28 May 1998 17:02:01 +0200 | wenzelm | changed get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option; | changeset | files |
| Thu, 28 May 1998 14:50:40 +0200 | wenzelm | tuned dist version; | changeset | files |
| Thu, 28 May 1998 12:24:05 +0200 | wenzelm | tuned header; | changeset | files |
| Thu, 28 May 1998 12:23:11 +0200 | wenzelm | version under control of Admin/makedist; | changeset | files |
| Thu, 28 May 1998 12:22:37 +0200 | wenzelm | README, Pure/ROOT.ML: version set automatically; | changeset | files |
| Thu, 28 May 1998 12:22:05 +0200 | wenzelm | version under control of Admin/makedist; | changeset | files |
| Thu, 28 May 1998 12:21:05 +0200 | wenzelm | added ml_prompts; | changeset | files |
| Thu, 28 May 1998 11:11:27 +0200 | wenzelm | added mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) | changeset | files |
| Thu, 28 May 1998 11:09:07 +0200 | wenzelm | tuned error msg; | changeset | files |
| Thu, 28 May 1998 11:08:45 +0200 | wenzelm | fixed error msgs; | changeset | files |
| Wed, 27 May 1998 12:25:56 +0200 | paulson | Structure Option now declared in MLWorks | changeset | files |
| Wed, 27 May 1998 12:23:45 +0200 | paulson | mk_all_imp: no longer creates goals that have beta-redexes | changeset | files |
| Wed, 27 May 1998 12:22:32 +0200 | paulson | more tracing | changeset | files |
| Wed, 27 May 1998 12:21:39 +0200 | paulson | Changed require to requires for MLWorks | changeset | files |
| Wed, 27 May 1998 12:19:35 +0200 | paulson | auto update | changeset | files |
| Tue, 26 May 1998 12:29:27 +0200 | wenzelm | made SML/NJ happy; | changeset | files |
| Tue, 26 May 1998 12:29:10 +0200 | wenzelm | foldl_map prep_field; | changeset | files |
| Mon, 25 May 1998 21:28:07 +0200 | wenzelm | tuned store_theory; | changeset | files |
| Mon, 25 May 1998 21:27:22 +0200 | wenzelm | tuned local, global; | changeset | files |
| Mon, 25 May 1998 21:25:04 +0200 | wenzelm | tuned store_theory: theory -> unit; | changeset | files |
| Mon, 25 May 1998 21:24:27 +0200 | wenzelm | added get_name, put_name, global_path, local_path, begin_theory, | changeset | files |
| Mon, 25 May 1998 21:17:08 +0200 | wenzelm | global_names moved to pure_thy.ML; | changeset | files |
| Mon, 25 May 1998 21:16:03 +0200 | wenzelm | certify_term: type_check replaces Term.type_of, providing sensible | changeset | files |
| Mon, 25 May 1998 21:14:00 +0200 | wenzelm | renamed state_source to source'; | changeset | files |
| Mon, 25 May 1998 21:13:20 +0200 | wenzelm | added recover, source; | changeset | files |
| Mon, 25 May 1998 21:12:46 +0200 | wenzelm | added catch: ('a -> 'b) -> 'a -> 'b; | changeset | files |
| Mon, 25 May 1998 21:11:46 +0200 | wenzelm | remove seq2, scan (use seq2, foldl_map from library.ML); | changeset | files |
| Mon, 25 May 1998 21:10:45 +0200 | wenzelm | added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list; | changeset | files |
| Mon, 25 May 1998 12:55:01 +0200 | nipkow | Swapped order of params. | changeset | files |
| Wed, 20 May 1998 18:58:13 +0200 | wenzelm | changed get_single: ('a, 'b) source -> 'a option * ('a, 'b) source; | changeset | files |
| Wed, 20 May 1998 18:57:16 +0200 | wenzelm | source vs. source'; | changeset | files |
| Wed, 20 May 1998 18:56:59 +0200 | wenzelm | tuned keywords; | changeset | files |
| Wed, 20 May 1998 18:56:36 +0200 | wenzelm | added is_stale; | changeset | files |
| Wed, 20 May 1998 18:56:00 +0200 | wenzelm | tuned signature; | changeset | files |
| Wed, 20 May 1998 18:55:41 +0200 | wenzelm | tuned comments; | changeset | files |
| Wed, 20 May 1998 18:55:16 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 20 May 1998 15:20:28 +0200 | nipkow | Small mods. | changeset | files |
| Tue, 19 May 1998 17:16:18 +0200 | wenzelm | prompt made part of source; | changeset | files |
| Tue, 19 May 1998 17:15:30 +0200 | wenzelm | fixed handle_error: cat_lines; | changeset | files |
| Tue, 19 May 1998 17:15:04 +0200 | wenzelm | added Thy/position.ML; | changeset | files |
| Tue, 19 May 1998 17:14:28 +0200 | wenzelm | added source: string -> (string, string list) Source.source; | changeset | files |
| Tue, 19 May 1998 17:14:01 +0200 | wenzelm | Input positions. | changeset | files |
| Mon, 18 May 1998 18:10:43 +0200 | wenzelm | added Syntax/source.ML; | changeset | files |
| Mon, 18 May 1998 18:10:04 +0200 | wenzelm | added Source module; | changeset | files |
| Mon, 18 May 1998 18:08:58 +0200 | wenzelm | Co-algebraic data sources. | changeset | files |
| Mon, 18 May 1998 17:57:47 +0200 | wenzelm | Symbol.stopper; | changeset | files |
| Mon, 18 May 1998 17:57:16 +0200 | wenzelm | improved finite scans: more abstract stopper; | changeset | files |
| Mon, 18 May 1998 17:31:58 +0200 | nipkow | snoc_induct/exhaust -> rev_induct_exhaust. | changeset | files |
| Mon, 18 May 1998 17:31:49 +0200 | nipkow | Cleaned up and simplified etc. | changeset | files |
| Fri, 15 May 1998 11:35:56 +0200 | wenzelm | witnesses: lookup stored thms instead of axioms; | changeset | files |
| Fri, 15 May 1998 11:34:49 +0200 | wenzelm | added add_axioms_x, add_defs_x; | changeset | files |
| Fri, 15 May 1998 11:34:12 +0200 | wenzelm | PureThy.add_typedecls; | changeset | files |
| Thu, 14 May 1998 16:54:20 +0200 | nipkow | Reordred arguments in AutoChopper. | changeset | files |
| Thu, 14 May 1998 16:50:09 +0200 | oheimb | extended addsplits and delsplits to handle also split rules for assumptions | changeset | files |
| Thu, 14 May 1998 16:44:04 +0200 | oheimb | simplifications | changeset | files |
| Thu, 14 May 1998 16:42:52 +0200 | oheimb | disabled (experimental) geometry option | changeset | files |
| Thu, 14 May 1998 16:35:30 +0200 | oheimb | keyboard settings now done by loading Tools/8bit/xemacs/isa_xemacs.emacs | changeset | files |
| Thu, 14 May 1998 16:32:33 +0200 | oheimb | added option_map_o_update | changeset | files |
| Wed, 13 May 1998 19:06:57 +0200 | wenzelm | added welcome; | changeset | files |
| Wed, 13 May 1998 19:06:14 +0200 | wenzelm | added :-- (dependent pair); | changeset | files |
| Wed, 13 May 1998 19:05:50 +0200 | wenzelm | added transform_error, exception ERROR_MESSAGE; | changeset | files |
| Wed, 13 May 1998 12:23:28 +0200 | wenzelm | added thms_closure: theory -> xstring -> tthm list option; | changeset | files |
| Wed, 13 May 1998 12:21:45 +0200 | wenzelm | adapted to new Scan.fail_with / Scan.!!; | changeset | files |
| Wed, 13 May 1998 12:20:53 +0200 | wenzelm | pure_nonterms; | changeset | files |
| Wed, 13 May 1998 12:20:28 +0200 | wenzelm | added fail_with and adapted !!; | changeset | files |
| Wed, 13 May 1998 12:19:01 +0200 | wenzelm | gen_attr: fixed order of evaluation; | changeset | files |
| Wed, 13 May 1998 12:17:49 +0200 | wenzelm | tuned msg; | changeset | files |
| Wed, 13 May 1998 12:17:30 +0200 | wenzelm | get_first: ('a -> 'b option) -> 'a list -> 'b option; | changeset | files |
| Wed, 13 May 1998 10:21:28 +0200 | wenzelm | HOL/record: now includes concrete syntax for record terms; | changeset | files |
| Tue, 12 May 1998 18:07:03 +0200 | wenzelm | added Goal, Goalw; | changeset | files |
| Tue, 12 May 1998 18:06:27 +0200 | wenzelm | branching_level = 250; | changeset | files |
| Tue, 12 May 1998 18:06:01 +0200 | wenzelm | fixed comment; | changeset | files |
| Tue, 12 May 1998 08:36:07 +0200 | nipkow | Removed duplicate list_length_induct | changeset | files |
| Mon, 11 May 1998 14:40:40 +0200 | nipkow | Reordered a few parameters. | changeset | files |
| Mon, 11 May 1998 13:18:25 +0200 | nipkow | Lex | changeset | files |
| Sun, 10 May 1998 11:59:31 +0200 | wenzelm | tuned comment; | changeset | files |
| Fri, 08 May 1998 18:33:29 +0200 | nipkow | Reshuffeling, renaming and a few simple corollaries. | changeset | files |
| Fri, 08 May 1998 15:45:01 +0200 | wenzelm | fixed translations; | changeset | files |
| Fri, 08 May 1998 13:54:45 +0200 | wenzelm | proper thy files; | changeset | files |
| Fri, 08 May 1998 10:15:39 +0200 | wenzelm | fixed update syntax; | changeset | files |
| Thu, 07 May 1998 18:34:48 +0200 | wenzelm | improved source: state-based; | changeset | files |
| Thu, 07 May 1998 18:05:46 +0200 | wenzelm | added scan_tvar; | changeset | files |
| Thu, 07 May 1998 18:05:08 +0200 | wenzelm | added 'space'; | changeset | files |
| Thu, 07 May 1998 13:02:23 +0200 | nipkow | Got rid of NAe.delta | changeset | files |
| Wed, 06 May 1998 13:01:45 +0200 | paulson | HOL/Update | changeset | files |
| Wed, 06 May 1998 13:01:30 +0200 | paulson | Removed some traces of UNITY | changeset | files |
| Wed, 06 May 1998 11:46:00 +0200 | nipkow | Changed [/] to [:=] and removed actual definition. | changeset | files |
| Tue, 05 May 1998 17:28:22 +0200 | paulson | New syntax for function update; moved to main HOL directory | changeset | files |
| Tue, 05 May 1998 13:27:18 +0200 | wenzelm | misc tuning; | changeset | files |
| Mon, 04 May 1998 21:07:57 +0200 | wenzelm | 'more' selector; | changeset | files |
| Mon, 04 May 1998 21:05:38 +0200 | wenzelm | added nth_update: 'a -> int * 'a list -> 'a list; | changeset | files |
| Mon, 04 May 1998 21:05:14 +0200 | wenzelm | tuned msg; | changeset | files |
| Mon, 04 May 1998 13:48:47 +0200 | wenzelm | fixed constdefs syntax; | changeset | files |