| Thu, 06 Nov 1997 10:28:20 +0100 | paulson | subgoal_tac displays a warning if the new subgoal has type variables | changeset | files |
| Wed, 05 Nov 1997 19:40:50 +0100 | wenzelm | mkdir -p bin; | changeset | files |
| Wed, 05 Nov 1997 19:39:34 +0100 | wenzelm | Tools/8bit: ./mk; | changeset | files |
| Wed, 05 Nov 1997 18:31:14 +0100 | oheimb | *** empty log message *** | changeset | files |
| Wed, 05 Nov 1997 16:37:22 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 05 Nov 1997 15:49:38 +0100 | oheimb | abandoned generation of tmp files | changeset | files |
| Wed, 05 Nov 1997 15:48:24 +0100 | oheimb | various improvements | changeset | files |
| Wed, 05 Nov 1997 15:47:27 +0100 | oheimb | reflecting changes of isa2latex | changeset | files |
| Wed, 05 Nov 1997 15:45:51 +0100 | oheimb | several minor improvements | changeset | files |
| Wed, 05 Nov 1997 15:42:30 +0100 | oheimb | added ax2isa | changeset | files |
| Wed, 05 Nov 1997 15:42:07 +0100 | oheimb | added ax2isa | changeset | files |
| Wed, 05 Nov 1997 15:38:40 +0100 | oheimb | added isabelle14 and isabelle24 | changeset | files |
| Wed, 05 Nov 1997 15:36:54 +0100 | oheimb | removed gererated files | changeset | files |
| Wed, 05 Nov 1997 15:36:40 +0100 | oheimb | added entry for manual | changeset | files |
| Wed, 05 Nov 1997 15:36:01 +0100 | oheimb | *** empty log message *** | changeset | files |
| Wed, 05 Nov 1997 14:00:49 +0100 | paulson | Now introduces Safe_tac | changeset | files |
| Wed, 05 Nov 1997 13:50:59 +0100 | paulson | Ran expandshort, especially to introduce Safe_tac | changeset | files |
| Wed, 05 Nov 1997 13:50:16 +0100 | paulson | Adapted to removal of UN1_I, etc | changeset | files |
| Wed, 05 Nov 1997 13:45:01 +0100 | paulson | Adapted to removal of UN1_I, etc | changeset | files |
| Wed, 05 Nov 1997 13:32:07 +0100 | paulson | UNIV now a constant; UNION1, INTER1 now translations and no longer have | changeset | files |
| Wed, 05 Nov 1997 13:29:47 +0100 | paulson | Expandshort; new theorem le_square | changeset | files |
| Wed, 05 Nov 1997 13:27:58 +0100 | paulson | generalized UNION1 to UNION | changeset | files |
| Wed, 05 Nov 1997 13:27:29 +0100 | paulson | Tidied Key_supply3 | changeset | files |
| Wed, 05 Nov 1997 13:26:19 +0100 | paulson | fixed comment | changeset | files |
| Wed, 05 Nov 1997 13:25:34 +0100 | paulson | UNIV & UNION1 | changeset | files |
| Wed, 05 Nov 1997 13:23:46 +0100 | paulson | Ran expandshort, especially to introduce Safe_tac | changeset | files |
| Wed, 05 Nov 1997 13:14:15 +0100 | paulson | Ran expandshort, especially to introduce Safe_tac | changeset | files |
| Wed, 05 Nov 1997 11:49:34 +0100 | wenzelm | adapted typed_print_translation; | changeset | files |
| Wed, 05 Nov 1997 11:49:07 +0100 | wenzelm | tuned record_info; | changeset | files |
| Wed, 05 Nov 1997 11:45:51 +0100 | wenzelm | fixed exception OPTION; | changeset | files |
| Wed, 05 Nov 1997 11:43:37 +0100 | wenzelm | adapted pure_trfunsT; | changeset | files |
| Wed, 05 Nov 1997 11:42:19 +0100 | wenzelm | print translation: added show_sorts argument; | changeset | files |
| Wed, 05 Nov 1997 11:41:46 +0100 | wenzelm | adapted syn_ext_trfunsT; | changeset | files |
| Wed, 05 Nov 1997 11:41:18 +0100 | wenzelm | adapted extend_trfunsT; | changeset | files |
| Wed, 05 Nov 1997 11:40:51 +0100 | wenzelm | fixed exception OPTION; | changeset | files |
| Wed, 05 Nov 1997 11:40:23 +0100 | wenzelm | added TYPE syntax; | changeset | files |
| Wed, 05 Nov 1997 11:35:07 +0100 | wenzelm | fixed exception OPTION; | changeset | files |
| Wed, 05 Nov 1997 11:34:44 +0100 | wenzelm | adapted add_trfunsT; | changeset | files |
| Wed, 05 Nov 1997 11:33:45 +0100 | wenzelm | adapted add_trfunsT; | changeset | files |
| Wed, 05 Nov 1997 11:33:05 +0100 | wenzelm | fixed exception OPTION; | changeset | files |
| Wed, 05 Nov 1997 11:19:15 +0100 | wenzelm | base root = ""; | changeset | files |
| Wed, 05 Nov 1997 09:08:35 +0100 | nipkow | Added an alternativ version of AutoChopper and a theory for the conversion of | changeset | files |
| Tue, 04 Nov 1997 20:52:20 +0100 | oheimb | removed redundant ball_image | changeset | files |
| Tue, 04 Nov 1997 20:50:35 +0100 | oheimb | removed redundant ball_empty and bex_empty (see equalities.ML) | changeset | files |
| Tue, 04 Nov 1997 20:49:45 +0100 | oheimb | added several theorems | changeset | files |
| Tue, 04 Nov 1997 20:48:38 +0100 | oheimb | added the, option_map, and case analysis theorems | changeset | files |
| Tue, 04 Nov 1997 20:47:38 +0100 | oheimb | added zip and nodup | changeset | files |
| Tue, 04 Nov 1997 20:46:56 +0100 | oheimb | added theorems for Eps | changeset | files |
| Tue, 04 Nov 1997 17:16:26 +0100 | wenzelm | tuned usage; | changeset | files |
| Tue, 04 Nov 1997 17:12:13 +0100 | wenzelm | HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML; | changeset | files |
| Tue, 04 Nov 1997 16:57:52 +0100 | wenzelm | tuned to make non-Poly/MLs happy; | changeset | files |
| Tue, 04 Nov 1997 16:49:35 +0100 | wenzelm | tuned 'records' stuff; | changeset | files |
| Tue, 04 Nov 1997 16:46:02 +0100 | wenzelm | added pretty_ctyp; | changeset | files |
| Tue, 04 Nov 1997 16:21:52 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 04 Nov 1997 16:17:04 +0100 | wenzelm | type object = exn (enhance readability); | changeset | files |
| Tue, 04 Nov 1997 15:16:23 +0100 | oheimb | *** empty log message *** | changeset | files |
| Tue, 04 Nov 1997 14:40:29 +0100 | oheimb | * removed "axioms" and "generated by" section | changeset | files |
| Tue, 04 Nov 1997 14:37:51 +0100 | oheimb | simplified (and corrected) syntax definition of fapp | changeset | files |
| Tue, 04 Nov 1997 14:09:37 +0100 | narasche | data kinds 'datatypes', data kinds 'records' added | changeset | files |
| Tue, 04 Nov 1997 13:35:13 +0100 | wenzelm | removed old datatype_info; | changeset | files |
| Tue, 04 Nov 1997 13:31:14 +0100 | wenzelm | added Thy/path.ML; | changeset | files |
| Tue, 04 Nov 1997 12:59:01 +0100 | nipkow | Logic.loops -> Logic.rewrite_rule_ok | changeset | files |
| Tue, 04 Nov 1997 12:58:10 +0100 | nipkow | logic: loops -> rewrite_rule_ok | changeset | files |
| Tue, 04 Nov 1997 12:46:50 +0100 | wenzelm | added path.ML; | changeset | files |
| Tue, 04 Nov 1997 12:44:17 +0100 | wenzelm | added base; | changeset | files |
| Tue, 04 Nov 1997 12:33:51 +0100 | wenzelm | Abstract algebra of file paths. External representation Unix-style. | changeset | files |
| Tue, 04 Nov 1997 12:04:57 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 04 Nov 1997 12:03:48 +0100 | wenzelm | removed old thy data stuff; | changeset | files |
| Tue, 04 Nov 1997 09:27:32 +0100 | wenzelm | fixed set_current_thy pattern; | changeset | files |
| Tue, 04 Nov 1997 09:26:15 +0100 | wenzelm | isatool fixclasimp; | changeset | files |
| Mon, 03 Nov 1997 21:56:59 +0100 | wenzelm | isatool fixclasimp; | changeset | files |
| Mon, 03 Nov 1997 21:15:08 +0100 | wenzelm | adapted to new datatypes thy info; | changeset | files |
| Mon, 03 Nov 1997 21:13:24 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 03 Nov 1997 21:12:40 +0100 | wenzelm | datatypes; | changeset | files |
| Mon, 03 Nov 1997 21:12:21 +0100 | wenzelm | nat datatype_info moved to Nat.thy; | changeset | files |
| Mon, 03 Nov 1997 21:04:51 +0100 | wenzelm | added MLtext section; | changeset | files |
| Mon, 03 Nov 1997 17:56:39 +0100 | wenzelm | added distinct_fst_string; | changeset | files |
| Mon, 03 Nov 1997 17:55:55 +0100 | wenzelm | tuned: distinct_fst_string; | changeset | files |
| Mon, 03 Nov 1997 14:37:35 +0100 | wenzelm | isatool fixclasimp; | changeset | files |
| Mon, 03 Nov 1997 14:09:16 +0100 | wenzelm | export const_decls parser; | changeset | files |
| Mon, 03 Nov 1997 14:06:27 +0100 | wenzelm | isatool fixclasimp; | changeset | files |
| Mon, 03 Nov 1997 12:36:48 +0100 | wenzelm | CLASET'; | changeset | files |
| Mon, 03 Nov 1997 12:28:45 +0100 | wenzelm | moved cladata.ML, simpdata.ML to ROOT.ML; | changeset | files |
| Mon, 03 Nov 1997 12:28:14 +0100 | wenzelm | adapted to new implicit claset; | changeset | files |
| Mon, 03 Nov 1997 12:28:01 +0100 | wenzelm | adapted to new implicit simpset; | changeset | files |
| Mon, 03 Nov 1997 12:26:58 +0100 | wenzelm | added claset thy_data; | changeset | files |
| Mon, 03 Nov 1997 12:26:45 +0100 | wenzelm | added simpset thy_data; | changeset | files |
| Mon, 03 Nov 1997 12:24:13 +0100 | wenzelm | isatool fixclasimp; | changeset | files |
| Mon, 03 Nov 1997 12:22:43 +0100 | wenzelm | isatool fixclasimp; | changeset | files |
| Mon, 03 Nov 1997 12:13:18 +0100 | wenzelm | isatool fixclasimp; | changeset | files |
| Mon, 03 Nov 1997 12:12:10 +0100 | wenzelm | added thy_data; | changeset | files |
| Mon, 03 Nov 1997 12:11:34 +0100 | wenzelm | use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML; | changeset | files |
| Mon, 03 Nov 1997 12:09:37 +0100 | wenzelm | adapted to new implicit simpset; | changeset | files |
| Mon, 03 Nov 1997 12:09:20 +0100 | wenzelm | adapted to new implicit claset; | changeset | files |
| Mon, 03 Nov 1997 12:07:13 +0100 | wenzelm | fixed thy dependencies; | changeset | files |
| Mon, 03 Nov 1997 12:05:42 +0100 | wenzelm | aded thy_data; | changeset | files |
| Mon, 03 Nov 1997 12:04:38 +0100 | wenzelm | HOL theory data. | changeset | files |
| Mon, 03 Nov 1997 12:03:13 +0100 | wenzelm | added thy_data.ML; | changeset | files |
| Mon, 03 Nov 1997 11:56:53 +0100 | wenzelm | new implicit simpset mechanism based on Sign.sg anytype data; | changeset | files |
| Mon, 03 Nov 1997 11:56:36 +0100 | wenzelm | new implicit claset mechanism based on Sign.sg anytype data; | changeset | files |
| Mon, 03 Nov 1997 11:56:17 +0100 | wenzelm | adapted to new implicit claset mechanism; | changeset | files |
| Mon, 03 Nov 1997 11:48:56 +0100 | wenzelm | fix references to implicit claset and simpset; | changeset | files |
| Mon, 03 Nov 1997 11:48:29 +0100 | wenzelm | do not overwrite backup files; | changeset | files |
| Mon, 03 Nov 1997 11:48:02 +0100 | wenzelm | set_session renamed to add_session; | changeset | files |
| Mon, 03 Nov 1997 11:46:42 +0100 | wenzelm | tuned error msg; | changeset | files |
| Mon, 03 Nov 1997 11:46:25 +0100 | wenzelm | made SML/97 happy; | changeset | files |
| Mon, 03 Nov 1997 09:58:06 +0100 | nipkow | expand_option_bind -> split_option_bind | changeset | files |
| Mon, 03 Nov 1997 09:57:35 +0100 | nipkow | expand_option_case -> split_option_case | changeset | files |
| Mon, 03 Nov 1997 08:16:35 +0100 | nipkow | *** empty log message *** | changeset | files |
| Mon, 03 Nov 1997 08:08:14 +0100 | nipkow | expand_list_case -> split_list_case | changeset | files |
| Sun, 02 Nov 1997 14:01:38 +0100 | nipkow | Indexed split_t_case. | changeset | files |
| Sun, 02 Nov 1997 13:47:58 +0100 | nipkow | Documented `split_t_case' thm genearted by datatype. | changeset | files |
| Sat, 01 Nov 1997 13:03:00 +0100 | paulson | Fixed comments | changeset | files |
| Sat, 01 Nov 1997 13:02:39 +0100 | paulson | New treatment of overloading\! | changeset | files |
| Sat, 01 Nov 1997 13:02:19 +0100 | paulson | New syntax function for types | changeset | files |
| Sat, 01 Nov 1997 13:01:57 +0100 | paulson | Faster lexing | changeset | files |
| Sat, 01 Nov 1997 13:01:07 +0100 | paulson | New way of referring to Basis Library | changeset | files |
| Sat, 01 Nov 1997 13:00:31 +0100 | paulson | mended type constraint\! | changeset | files |
| Sat, 01 Nov 1997 13:00:03 +0100 | paulson | Set.thy was too specific | changeset | files |
| Sat, 01 Nov 1997 12:59:06 +0100 | paulson | New Blast_tac (and minor tidying...) | changeset | files |