Fri, 07 Nov 1997 18:02:15 +0100 |
oheimb |
changed libraray function find to find_index_eq, currying it
|
changeset |
files
|
Fri, 07 Nov 1997 17:51:26 +0100 |
oheimb |
added contrapos
|
changeset |
files
|
Fri, 07 Nov 1997 17:51:10 +0100 |
oheimb |
added contrapos2
|
changeset |
files
|
Fri, 07 Nov 1997 15:24:58 +0100 |
oheimb |
added exists_Const
|
changeset |
files
|
Fri, 07 Nov 1997 08:25:02 +0100 |
nipkow |
Each datatype t now proves a theorem split_t_case_prem
|
changeset |
files
|
Thu, 06 Nov 1997 16:44:35 +0100 |
wenzelm |
Perl no longer optional;
|
changeset |
files
|
Thu, 06 Nov 1997 16:41:08 +0100 |
wenzelm |
deriv: eliminated references to theory;
|
changeset |
files
|
Thu, 06 Nov 1997 16:40:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 06 Nov 1997 12:27:12 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 06 Nov 1997 10:29:37 +0100 |
paulson |
hyp_subst_tac checks if the equality has type variables and uses a suitable
|
changeset |
files
|
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
|