| 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 |
| Sat, 01 Nov 1997 12:58:08 +0100 | paulson | Auto update | changeset | files |
| Sat, 01 Nov 1997 12:57:01 +0100 | wenzelm | propagate exn msg; | changeset | files |
| Fri, 31 Oct 1997 15:28:01 +0100 | wenzelm | dup sections: warning instead of error; | changeset | files |
| Fri, 31 Oct 1997 15:21:59 +0100 | wenzelm | Session, Context; | changeset | files |
| Fri, 31 Oct 1997 15:21:32 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 31 Oct 1997 15:20:20 +0100 | wenzelm | added mixfix_args; | changeset | files |
| Fri, 31 Oct 1997 15:19:50 +0100 | wenzelm | *** empty log message *** | changeset | files |
| Fri, 31 Oct 1997 15:15:06 +0100 | wenzelm | added str_of_sg: sg -> string; | changeset | files |
| Thu, 30 Oct 1997 17:05:20 +0100 | wenzelm | added mixfix_args; | changeset | files |
| Thu, 30 Oct 1997 17:04:54 +0100 | wenzelm | tuned thy_data; | changeset | files |
| Thu, 30 Oct 1997 17:01:50 +0100 | wenzelm | tuned init_data; | changeset | files |
| Thu, 30 Oct 1997 17:00:34 +0100 | wenzelm | added thy_data; | changeset | files |
| Thu, 30 Oct 1997 16:59:56 +0100 | wenzelm | added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option; | changeset | files |
| Thu, 30 Oct 1997 16:57:09 +0100 | nipkow | Modified trace output routines of simplifier. | changeset | files |
| Thu, 30 Oct 1997 14:19:17 +0100 | oheimb | domain package: | changeset | files |
| Thu, 30 Oct 1997 14:19:01 +0100 | oheimb | domain package: | changeset | files |
| Thu, 30 Oct 1997 14:18:14 +0100 | oheimb | domain package: | changeset | files |
| Thu, 30 Oct 1997 14:17:33 +0100 | oheimb | domain package: | changeset | files |
| Thu, 30 Oct 1997 11:43:32 +0100 | wenzelm | PureThy.add_store_defs_i, PureThy.add_store_axioms; | changeset | files |
| Thu, 30 Oct 1997 11:19:57 +0100 | wenzelm | fixed try_dest_adm; | changeset | files |
| Thu, 30 Oct 1997 10:50:04 +0100 | wenzelm | added adm.ML; | changeset | files |
| Thu, 30 Oct 1997 10:01:46 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 30 Oct 1997 09:59:38 +0100 | wenzelm | tuned simp trace; | changeset | files |
| Thu, 30 Oct 1997 09:54:47 +0100 | nipkow | *** empty log message *** | changeset | files |
| Thu, 30 Oct 1997 09:47:26 +0100 | nipkow | Removed spurious blank. | changeset | files |
| Thu, 30 Oct 1997 09:46:11 +0100 | nipkow | Updated proofs | changeset | files |
| Thu, 30 Oct 1997 09:45:03 +0100 | nipkow | For each datatype `t' there is now a theorem `split_t_case' of the form | changeset | files |
| Wed, 29 Oct 1997 16:03:19 +0100 | wenzelm | fixed spaces in qed; | changeset | files |
| Wed, 29 Oct 1997 14:23:49 +0100 | oheimb | debugging concerning sort variables | changeset | files |
| Tue, 28 Oct 1997 17:58:35 +0100 | wenzelm | PureThy.add_store_axioms_i; | changeset | files |
| Tue, 28 Oct 1997 17:58:08 +0100 | wenzelm | PureThy.add_store_defs_i, PureThy.add_store_axioms_i; | changeset | files |
| Tue, 28 Oct 1997 17:56:57 +0100 | wenzelm | PureThy.add_store_defs_i; | changeset | files |
| Tue, 28 Oct 1997 17:56:15 +0100 | wenzelm | PureThy.add_store_axioms; | changeset | files |
| Tue, 28 Oct 1997 17:41:40 +0100 | wenzelm | fixed qed; | changeset | files |
| Tue, 28 Oct 1997 17:41:15 +0100 | wenzelm | do not change global_names flag; | changeset | files |
| Tue, 28 Oct 1997 17:37:46 +0100 | wenzelm | restructured -- uses PureThy storage facilities; | changeset | files |
| Tue, 28 Oct 1997 17:36:16 +0100 | wenzelm | added ignored_consts, thms_containing, add_store_axioms(_i), | changeset | files |
| Tue, 28 Oct 1997 17:34:12 +0100 | wenzelm | always reload .ML *and* .thy file; | changeset | files |
| Tue, 28 Oct 1997 17:32:38 +0100 | wenzelm | PureThy.add_store_defs, PureThy.add_store_axioms; | changeset | files |
| Tue, 28 Oct 1997 17:31:55 +0100 | wenzelm | added ancestors; | changeset | files |
| Tue, 28 Oct 1997 17:30:47 +0100 | wenzelm | added name_of_thm; | changeset | files |
| Tue, 28 Oct 1997 17:29:48 +0100 | wenzelm | add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons, | changeset | files |
| Tue, 28 Oct 1997 17:28:11 +0100 | wenzelm | eq_thm moved to thm.ML; | changeset | files |
| Tue, 28 Oct 1997 17:27:10 +0100 | wenzelm | add_store_axioms_i; | changeset | files |
| Tue, 28 Oct 1997 14:03:25 +0100 | nipkow | Added finite_UNION/SigmaI. | changeset | files |
| Mon, 27 Oct 1997 16:01:53 +0100 | wenzelm | oops; | changeset | files |
| Mon, 27 Oct 1997 15:57:50 +0100 | wenzelm | renamed put_* to store_*; | changeset | files |
| Mon, 27 Oct 1997 15:43:53 +0100 | wenzelm | flipped global_names default; | changeset | files |
| Mon, 27 Oct 1997 15:43:16 +0100 | wenzelm | do not change global_names flag; | changeset | files |
| Mon, 27 Oct 1997 15:29:01 +0100 | wenzelm | Isa94-2 instead of Isa95; | changeset | files |
| Mon, 27 Oct 1997 11:34:33 +0100 | oheimb | adapted domain and ax_ops package for name spaces | changeset | files |
| Mon, 27 Oct 1997 10:46:36 +0100 | wenzelm | made SML/NJ happy; | changeset | files |
| Mon, 27 Oct 1997 10:34:17 +0100 | paulson | Deleted two needless theorems | changeset | files |
| Sat, 25 Oct 1997 14:43:55 +0200 | oheimb | internalized some names | changeset | files |
| Sat, 25 Oct 1997 14:39:25 +0200 | oheimb | corrected two comments | changeset | files |
| Fri, 24 Oct 1997 18:10:51 +0200 | nipkow | Added | changeset | files |
| Fri, 24 Oct 1997 18:02:23 +0200 | wenzelm | oops, swap warnings; | changeset | files |
| Fri, 24 Oct 1997 17:28:20 +0200 | wenzelm | record: tuned output; | changeset | files |
| Fri, 24 Oct 1997 17:25:33 +0200 | wenzelm | ProtoPure.flexpair_def; | changeset | files |
| Fri, 24 Oct 1997 17:19:14 +0200 | wenzelm | ProtoPure.flexpair_def; | changeset | files |
| Fri, 24 Oct 1997 17:18:49 +0200 | wenzelm | merge: default to ProtoPure.thy; | changeset | files |
| Fri, 24 Oct 1997 17:18:25 +0200 | wenzelm | ProtoPure.thy etc.; | changeset | files |
| Fri, 24 Oct 1997 17:18:00 +0200 | wenzelm | tuned names; | changeset | files |
| Fri, 24 Oct 1997 17:17:10 +0200 | wenzelm | self_ref: check_stale; | changeset | files |
| Fri, 24 Oct 1997 17:15:59 +0200 | wenzelm | eq_thm (from drule.ML); | changeset | files |
| Fri, 24 Oct 1997 17:14:41 +0200 | wenzelm | added declared: T -> string -> bool; | changeset | files |
| Fri, 24 Oct 1997 17:14:02 +0200 | wenzelm | Pure.thy; | changeset | files |
| Fri, 24 Oct 1997 17:13:21 +0200 | wenzelm | ProtoPure.thy; | changeset | files |
| Fri, 24 Oct 1997 17:12:35 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 24 Oct 1997 17:12:09 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 24 Oct 1997 17:11:48 +0200 | wenzelm | removed add_thms_as_axms; | changeset | files |
| Fri, 24 Oct 1997 17:11:23 +0200 | wenzelm | Init 'theorems' data. The Pure theories. | changeset | files |
| Fri, 24 Oct 1997 17:07:34 +0200 | wenzelm | added pure_thy.ML; | changeset | files |
| Fri, 24 Oct 1997 17:06:45 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 24 Oct 1997 11:56:12 +0200 | nipkow | Modified comment. | changeset | files |
| Fri, 24 Oct 1997 11:24:21 +0200 | nipkow | Deleted very odd Delsimps[Collect_False_empty] which made proofs fail! | changeset | files |
| Fri, 24 Oct 1997 11:05:21 +0200 | nipkow | HOL/Map | changeset | files |
| Fri, 24 Oct 1997 10:31:31 +0200 | nipkow | Added the new theory Map. | changeset | files |
| Thu, 23 Oct 1997 12:49:16 +0200 | wenzelm | added record section; | changeset | files |
| Thu, 23 Oct 1997 12:48:48 +0200 | wenzelm | Sign.name_of; | changeset | files |
| Thu, 23 Oct 1997 12:47:59 +0200 | wenzelm | Sign.stamp_names_of; | changeset | files |
| Thu, 23 Oct 1997 12:44:46 +0200 | wenzelm | improved typ parser, exported; | changeset | files |
| Thu, 23 Oct 1997 12:43:07 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 23 Oct 1997 12:13:15 +0200 | wenzelm | hide id, stamps; | changeset | files |
| Thu, 23 Oct 1997 12:10:55 +0200 | wenzelm | Sign.stamp_names_of; | changeset | files |
| Thu, 23 Oct 1997 12:10:32 +0200 | wenzelm | added sort_wrt; | changeset | files |
| Thu, 23 Oct 1997 12:09:48 +0200 | wenzelm | fixed prune of hidden short names; | changeset | files |
| Thu, 23 Oct 1997 12:09:31 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 22 Oct 1997 11:36:43 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 22 Oct 1997 11:36:29 +0200 | wenzelm | certify: check_stale; | changeset | files |
| Tue, 21 Oct 1997 18:15:43 +0200 | wenzelm | improved handling of draft signatures / theories; draft thms (and | changeset | files |
| Tue, 21 Oct 1997 18:09:13 +0200 | wenzelm | sg_ref: automatic adjustment of thms of draft theories; | changeset | files |
| Tue, 21 Oct 1997 17:48:06 +0200 | wenzelm | commit; | changeset | files |
| Tue, 21 Oct 1997 17:47:50 +0200 | wenzelm | made Poly/ML happy, but SML/NJ unhappy; | changeset | files |
| Tue, 21 Oct 1997 17:38:31 +0200 | nipkow | typo | changeset | files |
| Tue, 21 Oct 1997 17:36:54 +0200 | nipkow | Corrected alphabetical order of entries in signature. | changeset | files |
| Tue, 21 Oct 1997 10:52:25 +0200 | paulson | Fixed the index entries for "recursion, general" | changeset | files |
| Tue, 21 Oct 1997 10:39:27 +0200 | paulson | Many minor speedups: | changeset | files |
| Tue, 21 Oct 1997 10:36:23 +0200 | paulson | New rewrite rules image_iff | changeset | files |
| Mon, 20 Oct 1997 17:21:54 +0200 | nipkow | Documented `addsplits' | changeset | files |
| Mon, 20 Oct 1997 17:08:18 +0200 | wenzelm | make SML/NJ happy; | changeset | files |
| Mon, 20 Oct 1997 15:20:42 +0200 | wenzelm | rm IOA TLA; | changeset | files |
| Mon, 20 Oct 1997 15:20:20 +0200 | wenzelm | tuned types; | changeset | files |
| Mon, 20 Oct 1997 15:18:09 +0200 | wenzelm | tuned sig; | changeset | files |
| Mon, 20 Oct 1997 12:50:18 +0200 | wenzelm | reset global_names; | changeset | files |
| Mon, 20 Oct 1997 12:47:44 +0200 | wenzelm | set global_names; | changeset | files |
| Mon, 20 Oct 1997 12:47:02 +0200 | wenzelm | replaced ops by consts; | changeset | files |
| Mon, 20 Oct 1997 12:45:51 +0200 | wenzelm | removed Dlist; | changeset | files |
| Mon, 20 Oct 1997 11:53:42 +0200 | nipkow | \label{simp-chap} -> chap:simplification | changeset | files |
| Mon, 20 Oct 1997 11:47:04 +0200 | wenzelm | fixed goal_XXX; | changeset | files |
| Mon, 20 Oct 1997 11:39:29 +0200 | wenzelm | adapted to qualified names; | changeset | files |
| Mon, 20 Oct 1997 11:25:39 +0200 | wenzelm | adapted to qualified names; | changeset | files |
| Mon, 20 Oct 1997 11:22:29 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 20 Oct 1997 11:14:55 +0200 | wenzelm | adapted to qualified names; | changeset | files |
| Mon, 20 Oct 1997 11:14:16 +0200 | wenzelm | lookup long names of types; | changeset | files |
| Mon, 20 Oct 1997 11:08:29 +0200 | wenzelm | tuned qualified names; | changeset | files |
| Mon, 20 Oct 1997 11:06:01 +0200 | wenzelm | adapted to qualified names; | changeset | files |
| Mon, 20 Oct 1997 11:01:07 +0200 | wenzelm | qualified names; | changeset | files |
| Mon, 20 Oct 1997 10:53:42 +0200 | wenzelm | local; | changeset | files |
| Mon, 20 Oct 1997 10:53:25 +0200 | wenzelm | Sign.base_name; | changeset | files |
| Mon, 20 Oct 1997 10:52:32 +0200 | wenzelm | fixed types of add_XXX; | changeset | files |
| Mon, 20 Oct 1997 10:52:04 +0200 | wenzelm | fixed types of add_XXX; | changeset | files |
| Mon, 20 Oct 1997 10:51:01 +0200 | wenzelm | tuned output; | changeset | files |
| Mon, 20 Oct 1997 10:48:22 +0200 | wenzelm | adapted to qualified names; | changeset | files |
| Mon, 20 Oct 1997 10:39:26 +0200 | wenzelm | Sign.base_name; | changeset | files |
| Mon, 20 Oct 1997 10:39:04 +0200 | wenzelm | fixed types of add_XXX; | changeset | files |
| Mon, 20 Oct 1997 10:38:36 +0200 | wenzelm | local; | changeset | files |
| Mon, 20 Oct 1997 10:38:16 +0200 | wenzelm | local section; | changeset | files |
| Sat, 18 Oct 1997 13:23:02 +0200 | nipkow | addsplits | changeset | files |
| Fri, 17 Oct 1997 19:07:56 +0200 | wenzelm | adapted to qualified names; | changeset | files |
| Fri, 17 Oct 1997 18:19:14 +0200 | wenzelm | no longer tries bogus eta-contract involving aprops; | changeset | files |
| Fri, 17 Oct 1997 18:14:48 +0200 | wenzelm | adapted to qualified names; | changeset | files |
| Fri, 17 Oct 1997 18:03:46 +0200 | wenzelm | fixed RAW target; | changeset | files |
| Fri, 17 Oct 1997 17:42:39 +0200 | wenzelm | (co) inductive / datatype package adapted to qualified names; | changeset | files |
| Fri, 17 Oct 1997 17:40:33 +0200 | wenzelm | obselete 'end' hack; | changeset | files |
| Fri, 17 Oct 1997 17:40:02 +0200 | wenzelm | global; | changeset | files |
| Fri, 17 Oct 1997 17:39:04 +0200 | wenzelm | tuned "." syntax; | changeset | files |
| Fri, 17 Oct 1997 17:33:22 +0200 | wenzelm | removed Classlib; | changeset | files |
| Fri, 17 Oct 1997 17:32:27 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Fri, 17 Oct 1997 15:25:12 +0200 | nipkow | setloop split_tac -> addsplits | changeset | files |
| Fri, 17 Oct 1997 15:23:14 +0200 | nipkow | Added error messages. | changeset | files |
| Fri, 17 Oct 1997 11:12:36 +0200 | paulson | A lot of new comments | changeset | files |
| Fri, 17 Oct 1997 11:10:54 +0200 | paulson | Eta-expanded a function decl to make sml/nj happy | changeset | files |
| Fri, 17 Oct 1997 11:10:13 +0200 | paulson | Added "op" before "occs" to make sml/nj happy | changeset | files |
| Fri, 17 Oct 1997 11:09:34 +0200 | paulson | New rewrite rules for simplifying conditionals | changeset | files |
| Fri, 17 Oct 1997 11:00:50 +0200 | paulson | New trivial rewrites | changeset | files |
| Fri, 17 Oct 1997 11:00:00 +0200 | paulson | New rewrite rules for simplifying conditionals | changeset | files |
| Fri, 17 Oct 1997 10:58:44 +0200 | paulson | Better simplification eliminates a command from proof of psubset_card | changeset | files |
| Fri, 17 Oct 1997 10:57:48 +0200 | paulson | New simprules imp_disj1,2 and some comments | changeset | files |
| Fri, 17 Oct 1997 09:04:02 +0200 | nipkow | Added image_eqI to simpset. | changeset | files |
| Fri, 17 Oct 1997 09:03:16 +0200 | nipkow | Removed image_eqI from simpset because of clash with neq_shrK. | changeset | files |
| Thu, 16 Oct 1997 16:54:31 +0200 | nipkow | AddIffs [all_not_in_conv]; | changeset | files |
| Thu, 16 Oct 1997 15:33:06 +0200 | wenzelm | global; | changeset | files |
| Thu, 16 Oct 1997 15:31:12 +0200 | nipkow | Modified comment. | changeset | files |
| Thu, 16 Oct 1997 15:23:53 +0200 | paulson | New simprules imp_disj1, imp_disj2 | changeset | files |
| Thu, 16 Oct 1997 15:23:25 +0200 | paulson | New simprule diff_le_self, requiring a new proof of diff_diff_cancel | changeset | files |
| Thu, 16 Oct 1997 15:09:08 +0200 | nipkow | Removed comment. | changeset | files |
| Thu, 16 Oct 1997 14:52:35 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 16 Oct 1997 14:48:10 +0200 | wenzelm | removed begin; | changeset | files |
| Thu, 16 Oct 1997 14:46:55 +0200 | wenzelm | fixed prep_ext; | changeset | files |
| Thu, 16 Oct 1997 14:14:01 +0200 | nipkow | Simplified proof. | changeset | files |
| Thu, 16 Oct 1997 14:12:58 +0200 | nipkow | Simplified proof because of better simplifier. | changeset | files |
| Thu, 16 Oct 1997 14:12:15 +0200 | nipkow | Various new lemmas. Improved conversion of equations to rewrite rules: | changeset | files |
| Thu, 16 Oct 1997 14:00:20 +0200 | wenzelm | added transfer: theory -> thm -> thm; | changeset | files |
| Thu, 16 Oct 1997 13:45:27 +0200 | wenzelm | oops; | changeset | files |
| Thu, 16 Oct 1997 13:45:16 +0200 | nipkow | The simplifier has been improved a little: equations s=t which used to be | changeset | files |
| Thu, 16 Oct 1997 13:43:42 +0200 | wenzelm | fixed dependencies; | changeset | files |
| Thu, 16 Oct 1997 13:42:53 +0200 | wenzelm | transfer thy Ord_nat; | changeset | files |
| Thu, 16 Oct 1997 13:42:29 +0200 | wenzelm | sevaral goals restated in mono.thy; | changeset | files |
| Thu, 16 Oct 1997 13:39:20 +0200 | wenzelm | moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML; | changeset | files |
| Thu, 16 Oct 1997 13:38:47 +0200 | wenzelm | transfer InfDatatype.thy Limit_VfromE; | changeset | files |
| Thu, 16 Oct 1997 13:38:28 +0200 | wenzelm | transfer CardinalArith.thy nat_into_Ord; | changeset | files |
| Thu, 16 Oct 1997 13:36:04 +0200 | wenzelm | improved pretty_arity; | changeset | files |
| Thu, 16 Oct 1997 13:34:15 +0200 | wenzelm | added merge_theories (new name arg); | changeset | files |
| Thu, 16 Oct 1997 13:33:17 +0200 | wenzelm | fixed merge_theories; | changeset | files |
| Thu, 16 Oct 1997 13:28:04 +0200 | wenzelm | revert to 1.3; | changeset | files |
| Thu, 16 Oct 1997 13:20:31 +0200 | wenzelm | revert to 1.1; | changeset | files |
| Thu, 16 Oct 1997 13:13:03 +0200 | nipkow | Added last, butlast, dropped ttl. | changeset | files |
| Thu, 16 Oct 1997 10:29:56 +0200 | mueller | lala | changeset | files |
| Thu, 16 Oct 1997 10:22:37 +0200 | paulson | Eta-expansion of function declarations, for value polymorphism | changeset | files |
| Wed, 15 Oct 1997 15:18:41 +0200 | wenzelm | remove merge_theories; | changeset | files |
| Wed, 15 Oct 1997 15:17:32 +0200 | wenzelm | make_draft replaced by prep_ext; | changeset | files |
| Wed, 15 Oct 1997 15:15:22 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 15 Oct 1997 15:14:56 +0200 | wenzelm | eliminated aliasing merge: now always extends; | changeset | files |
| Wed, 15 Oct 1997 15:13:43 +0200 | wenzelm | tuned comment; | changeset | files |
| Wed, 15 Oct 1997 15:13:25 +0200 | wenzelm | improved print_data; | changeset | files |
| Wed, 15 Oct 1997 15:12:59 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 15 Oct 1997 11:43:27 +0200 | wenzelm | slightly changed interfaces for oracles; | changeset | files |
| Wed, 15 Oct 1997 11:27:55 +0200 | nipkow | Added ack to Mateja Jamnik. | changeset | files |
| Wed, 15 Oct 1997 11:16:48 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 14 Oct 1997 17:36:45 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 14 Oct 1997 17:36:22 +0200 | wenzelm | added additional generic data; | changeset | files |
| Tue, 14 Oct 1997 17:35:56 +0200 | wenzelm | Sign.print_data; | changeset | files |
| Tue, 14 Oct 1997 17:35:35 +0200 | wenzelm | added init_data, get_data, put_data; | changeset | files |
| Tue, 14 Oct 1997 17:34:36 +0200 | wenzelm | added data.ML; | changeset | files |
| Tue, 14 Oct 1997 17:34:21 +0200 | wenzelm | Arbitrarily typed data. | changeset | files |
| Tue, 14 Oct 1997 17:23:01 +0200 | paulson | Patch to avoid simplification of ~EX to ALL~ | changeset | files |
| Tue, 14 Oct 1997 13:59:12 +0200 | nipkow | Two lemmas are already in List. | changeset | files |
| Tue, 14 Oct 1997 13:58:47 +0200 | nipkow | More lemmas, esp. ~Bex and ~Ball conversions. | changeset | files |
| Tue, 14 Oct 1997 12:41:11 +0200 | nipkow | Added neagtion rules for Ball and Bex. | changeset | files |
| Tue, 14 Oct 1997 11:57:14 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 14 Oct 1997 11:30:35 +0200 | wenzelm | browser info; | changeset | files |
| Tue, 14 Oct 1997 10:52:17 +0200 | paulson | rearranged and added TLA | changeset | files |
| Mon, 13 Oct 1997 17:49:50 +0200 | wenzelm | fixed extern; | changeset | files |
| Mon, 13 Oct 1997 17:49:08 +0200 | wenzelm | uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity; | changeset | files |
| Mon, 13 Oct 1997 17:47:59 +0200 | wenzelm | uses Sign.str_of_sort; | changeset | files |
| Mon, 13 Oct 1997 12:51:51 +0200 | wenzelm | fixed dots; | changeset | files |
| Mon, 13 Oct 1997 12:48:42 +0200 | wenzelm | print_goals: optional output of const types (set show_consts); | changeset | files |
| Mon, 13 Oct 1997 12:48:23 +0200 | wenzelm | merge: drops path elements; | changeset | files |
| Mon, 13 Oct 1997 11:00:06 +0200 | merz | Absolute URL's for documentation | changeset | files |
| Mon, 13 Oct 1997 10:31:21 +0200 | wenzelm | non-transparent logo; | changeset | files |
| Mon, 13 Oct 1997 10:22:28 +0200 | wenzelm | fixed dots; | changeset | files |
| Mon, 13 Oct 1997 10:14:52 +0200 | wenzelm | hierachically structured name spaces; | changeset | files |
| Sun, 12 Oct 1997 22:06:00 +0200 | berghofe | Changed logo. | changeset | files |
| Sun, 12 Oct 1997 22:04:06 +0200 | berghofe | Added command for copying new logo. | changeset | files |
| Fri, 10 Oct 1997 19:13:58 +0200 | wenzelm | fixed dots; | changeset | files |
| Fri, 10 Oct 1997 19:02:28 +0200 | wenzelm | fixed dots; | changeset | files |
| Fri, 10 Oct 1997 18:37:49 +0200 | wenzelm | fixed fixed dots; | changeset | files |
| Fri, 10 Oct 1997 18:23:31 +0200 | wenzelm | fixed dots; | changeset | files |
| Fri, 10 Oct 1997 18:17:17 +0200 | wenzelm | fixed dots; | changeset | files |
| Fri, 10 Oct 1997 17:38:50 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 10 Oct 1997 17:10:12 +0200 | wenzelm | fixed dots; | changeset | files |
| Fri, 10 Oct 1997 16:29:41 +0200 | wenzelm | fixed dots; | changeset | files |
| Fri, 10 Oct 1997 15:52:12 +0200 | wenzelm | fixed dots; | changeset | files |
| Fri, 10 Oct 1997 15:51:38 +0200 | wenzelm | BAD_space_explode; | changeset | files |
| Fri, 10 Oct 1997 15:51:14 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 10 Oct 1997 15:50:46 +0200 | wenzelm | fixed space_explode, old one retained as BAD_space_explode; | changeset | files |
| Fri, 10 Oct 1997 15:48:43 +0200 | wenzelm | scan_longid moved to Syntax/lexicon.ML; | changeset | files |
| Fri, 10 Oct 1997 15:48:10 +0200 | wenzelm | constify: qualified is const; | changeset | files |
| Fri, 10 Oct 1997 15:47:41 +0200 | wenzelm | added longid syntax; | changeset | files |
| Fri, 10 Oct 1997 15:46:50 +0200 | wenzelm | added longid; | changeset | files |
| Fri, 10 Oct 1997 15:44:48 +0200 | wenzelm | decode: qualified is always const; | changeset | files |
| Fri, 10 Oct 1997 14:51:58 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 09 Oct 1997 18:01:27 +0200 | wenzelm | \n at end; | changeset | files |
| Thu, 09 Oct 1997 17:45:03 +0200 | wenzelm | ensure that dots in formulas are followed by non-idents; | changeset | files |
| Thu, 09 Oct 1997 17:20:15 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Thu, 09 Oct 1997 15:06:49 +0200 | wenzelm | no longer handles consts "" -- use syntax instead; | changeset | files |
| Thu, 09 Oct 1997 15:04:21 +0200 | wenzelm | removed open; | changeset | files |
| Thu, 09 Oct 1997 15:03:06 +0200 | wenzelm | fixed infix syntax; | changeset | files |
| Thu, 09 Oct 1997 15:01:11 +0200 | wenzelm | added TLA stuff; | changeset | files |
| Thu, 09 Oct 1997 15:00:41 +0200 | wenzelm | fixed oracle; | changeset | files |
| Thu, 09 Oct 1997 14:59:36 +0200 | wenzelm | removed declIffOracle; | changeset | files |
| Thu, 09 Oct 1997 14:56:52 +0200 | wenzelm | changed preference order of prtab entries; | changeset | files |
| Thu, 09 Oct 1997 14:55:24 +0200 | wenzelm | fixed infix syntax; | changeset | files |
| Thu, 09 Oct 1997 14:55:05 +0200 | wenzelm | improved oracles: named, many per theory; | changeset | files |
| Thu, 09 Oct 1997 14:53:31 +0200 | wenzelm | improved oracle: name; | changeset | files |
| Thu, 09 Oct 1997 14:52:36 +0200 | wenzelm | fixed get_axiom, invoke_oracle; | changeset | files |
| Thu, 09 Oct 1997 14:51:10 +0200 | wenzelm | print_theory: added oracles; | changeset | files |
| Thu, 09 Oct 1997 14:50:39 +0200 | wenzelm | tuned exports; | changeset | files |
| Thu, 09 Oct 1997 14:39:44 +0200 | wenzelm | fixed axiom names; | changeset | files |
| Wed, 08 Oct 1997 12:15:59 +0200 | wenzelm | symbols syntax; | changeset | files |
| Wed, 08 Oct 1997 11:50:33 +0200 | wenzelm | A formalization of TLA in HOL -- by Stephan Merz; | changeset | files |
| Tue, 07 Oct 1997 18:02:42 +0200 | wenzelm | improved types of add_XXX funs (xtyp etc.); | changeset | files |
| Tue, 07 Oct 1997 18:02:02 +0200 | wenzelm | improved types of add_XXX funs (xtyp etc.); | changeset | files |
| Tue, 07 Oct 1997 17:58:50 +0200 | wenzelm | tuned decode; | changeset | files |
| Tue, 07 Oct 1997 17:58:01 +0200 | wenzelm | tuned internal mapping table; | changeset | files |
| Tue, 07 Oct 1997 17:08:48 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 07 Oct 1997 17:06:05 +0200 | wenzelm | tuned warning msg; | changeset | files |
| Tue, 07 Oct 1997 12:37:53 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 07 Oct 1997 12:29:34 +0200 | wenzelm | The Isabelle Logo; | changeset | files |
| Mon, 06 Oct 1997 20:00:31 +0200 | wenzelm | fixed 'begin'; | changeset | files |
| Mon, 06 Oct 1997 19:39:40 +0200 | wenzelm | optional begin keyword; | changeset | files |
| Mon, 06 Oct 1997 19:16:57 +0200 | wenzelm | "->" made syntax; | changeset | files |
| Mon, 06 Oct 1997 19:15:22 +0200 | wenzelm | eliminated raise_term; | changeset | files |
| Mon, 06 Oct 1997 19:15:02 +0200 | wenzelm | eliminated raise_term, raise_typ; | changeset | files |
| Mon, 06 Oct 1997 19:13:55 +0200 | wenzelm | add_arities_i; | changeset | files |
| Mon, 06 Oct 1997 19:13:29 +0200 | wenzelm | TODO: handle internal / external names; | changeset | files |
| Mon, 06 Oct 1997 19:11:56 +0200 | wenzelm | now supports qualified names (intern vs. extern) !!! | changeset | files |
| Mon, 06 Oct 1997 19:07:14 +0200 | wenzelm | eliminated raise_term, raise_typ; | changeset | files |
| Mon, 06 Oct 1997 18:59:49 +0200 | wenzelm | tuned read_cterms; | changeset | files |
| Mon, 06 Oct 1997 18:57:17 +0200 | wenzelm | eliminated raise_term, raise_typ; | changeset | files |
| Mon, 06 Oct 1997 18:43:32 +0200 | wenzelm | new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i | changeset | files |
| Mon, 06 Oct 1997 18:41:39 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 06 Oct 1997 18:41:09 +0200 | wenzelm | now uses new Sign.pretty_sort; | changeset | files |
| Mon, 06 Oct 1997 18:40:24 +0200 | wenzelm | eliminated raise_term, raise_typ; | changeset | files |
| Mon, 06 Oct 1997 18:39:54 +0200 | wenzelm | now uses Syntax.simple_str_of_sort; | changeset | files |
| Mon, 06 Oct 1997 18:39:25 +0200 | wenzelm | added simple_str_of_sort; | changeset | files |
| Mon, 06 Oct 1997 18:29:43 +0200 | wenzelm | eliminated raise_term; | changeset | files |
| Mon, 06 Oct 1997 18:29:11 +0200 | wenzelm | added 'path' section; | changeset | files |
| Mon, 06 Oct 1997 18:27:55 +0200 | wenzelm | added pretty_sort; | changeset | files |
| Mon, 06 Oct 1997 18:25:04 +0200 | wenzelm | fixed raw_term_sorts (again!); | changeset | files |
| Mon, 06 Oct 1997 18:23:13 +0200 | wenzelm | eliminated raise_ast, raise_term, raise_typ; | changeset | files |
| Mon, 06 Oct 1997 18:22:22 +0200 | wenzelm | added sort_to_ast; | changeset | files |
| Mon, 06 Oct 1997 18:21:00 +0200 | wenzelm | eliminated raise_ast; | changeset | files |
| Mon, 06 Oct 1997 18:20:15 +0200 | wenzelm | RAW target; | changeset | files |
| Mon, 06 Oct 1997 09:26:00 +0200 | wenzelm | syntactic constants; | changeset | files |
| Fri, 03 Oct 1997 10:32:50 +0200 | paulson | Routine tidying up | changeset | files |
| Thu, 02 Oct 1997 22:54:00 +0200 | wenzelm | fully qualified names: Theory.add_XXX; | changeset | files |
| Wed, 01 Oct 1997 18:19:44 +0200 | wenzelm | fully qualified name: Theory.set_oracle; | changeset | files |
| Wed, 01 Oct 1997 18:19:18 +0200 | wenzelm | exported separator; | changeset | files |
| Wed, 01 Oct 1997 18:13:41 +0200 | wenzelm | fully qualified names: Theory.add_XXX; | changeset | files |
| Wed, 01 Oct 1997 17:43:42 +0200 | wenzelm | moved theory stuff (add_defs etc.) here from drule.ML; | changeset | files |
| Wed, 01 Oct 1997 17:42:32 +0200 | wenzelm | moved theory stuff (add_defs etc.) to theory.ML; | changeset | files |
| Wed, 01 Oct 1997 17:41:20 +0200 | wenzelm | fully qualified name: Theory.merge_thy_list; | changeset | files |
| Wed, 01 Oct 1997 17:40:09 +0200 | wenzelm | fully qualified names: Theory.add_XXX; | changeset | files |
| Wed, 01 Oct 1997 17:36:51 +0200 | wenzelm | added name_space.ML; | changeset | files |
| Wed, 01 Oct 1997 17:32:38 +0200 | wenzelm | added split_last; | changeset | files |
| Wed, 01 Oct 1997 14:30:38 +0200 | wenzelm | Hierarchically structured name spaces. | changeset | files |
| Wed, 01 Oct 1997 13:42:18 +0200 | paulson | Strengthened the possibility property for resumption so that it could have | changeset | files |
| Wed, 01 Oct 1997 13:41:38 +0200 | paulson | Fixed ServerResume to check for ServerHello instead of making a new NB | changeset | files |
| Wed, 01 Oct 1997 12:07:24 +0200 | paulson | Exchanged the M and SID fields of the FINISHED messages to simplify proofs; | changeset | files |
| Wed, 01 Oct 1997 12:07:07 +0200 | paulson | Exchanged the M and SID fields of the FINISHED messages to simplify proofs | changeset | files |
| Wed, 01 Oct 1997 11:30:55 +0200 | paulson | Auto update | changeset | files |
| Tue, 30 Sep 1997 17:33:16 +0200 | berghofe | SYNC | changeset | files |
| Tue, 30 Sep 1997 17:32:33 +0200 | berghofe | Removed "browse.tex". | changeset | files |
| Tue, 30 Sep 1997 17:31:19 +0200 | berghofe | Added section describing the theory browser. | changeset | files |
| Tue, 30 Sep 1997 17:29:32 +0200 | berghofe | Updated usage information for tool "usedir". | changeset | files |
| Tue, 30 Sep 1997 17:28:54 +0200 | berghofe | Theory browser stuff has been moved to "present.tex". | changeset | files |
| Tue, 30 Sep 1997 16:19:27 +0200 | wenzelm | obsolete; | changeset | files |
| Tue, 30 Sep 1997 16:12:38 +0200 | wenzelm | ISABELLE_USEDIR_OPTIONS="-i true" | changeset | files |
| Tue, 30 Sep 1997 12:53:54 +0200 | berghofe | Changed html data directory and names of graph files. | changeset | files |
| Tue, 30 Sep 1997 12:52:15 +0200 | berghofe | There is now one single option -i for generating theory browsing | changeset | files |
| Tue, 30 Sep 1997 12:49:16 +0200 | berghofe | Modified some links. | changeset | files |
| Tue, 30 Sep 1997 11:03:55 +0200 | paulson | Client, Server certificates now sent using the separate Certificate rule, | changeset | files |
| Mon, 29 Sep 1997 15:39:28 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 29 Sep 1997 15:16:22 +0200 | wenzelm | superficial; | changeset | files |
| Mon, 29 Sep 1997 15:11:27 +0200 | wenzelm | obsolete; | changeset | files |
| Mon, 29 Sep 1997 15:08:47 +0200 | wenzelm | margin 76 (2nd try :-); | changeset | files |
| Mon, 29 Sep 1997 14:12:02 +0200 | wenzelm | fixed href to html library; | changeset | files |
| Mon, 29 Sep 1997 14:11:18 +0200 | wenzelm | improved warning; | changeset | files |
| Mon, 29 Sep 1997 14:10:52 +0200 | wenzelm | default margin 76 (to accomodate warning and error default output); | changeset | files |
| Mon, 29 Sep 1997 12:13:43 +0200 | paulson | Step_tac -> Safe_tac | changeset | files |
| Mon, 29 Sep 1997 11:56:04 +0200 | paulson | Much tidying including step_tac -> clarify_tac or safe_tac; sometimes | changeset | files |
| Mon, 29 Sep 1997 11:52:25 +0200 | paulson | Step_tac -> Safe_tac | changeset | files |
| Mon, 29 Sep 1997 11:51:52 +0200 | paulson | Much tidying including "qed" instead of result(), and even qed_spec_mp, | changeset | files |
| Mon, 29 Sep 1997 11:51:09 +0200 | paulson | Previously loaded the WRONG THEORY, ignoring Confluence... | changeset | files |
| Mon, 29 Sep 1997 11:49:33 +0200 | paulson | Now using qed_spec_mp | changeset | files |
| Mon, 29 Sep 1997 11:48:48 +0200 | paulson | result() -> qed; Step_tac -> Safe_tac | changeset | files |
| Mon, 29 Sep 1997 11:47:01 +0200 | paulson | Step_tac -> Safe_tac | changeset | files |
| Mon, 29 Sep 1997 11:46:33 +0200 | paulson | Renamed XA, XB to PA, PB and removed the certificate from Client Verify | changeset | files |
| Mon, 29 Sep 1997 11:45:52 +0200 | paulson | Default simpset tactics now dereference "simpset" | changeset | files |
| Mon, 29 Sep 1997 11:44:56 +0200 | paulson | Added Safe_tac; all other default claset tactics now dereference "claset" | changeset | files |
| Mon, 29 Sep 1997 11:42:15 +0200 | paulson | fast_tac HOL_cs -> Fast_tac, etc. | changeset | files |
| Mon, 29 Sep 1997 11:40:03 +0200 | paulson | result() -> qed | changeset | files |
| Mon, 29 Sep 1997 11:37:02 +0200 | paulson | Step_tac -> Safe_tac | changeset | files |
| Mon, 29 Sep 1997 11:36:44 +0200 | paulson | Tidied proof of r_comp_rtrancl_eq | changeset | files |
| Mon, 29 Sep 1997 11:32:25 +0200 | paulson | qed_spec_mp, normalize_thm, etc. copied in from HOL.ML | changeset | files |
| Mon, 29 Sep 1997 11:31:56 +0200 | paulson | Step_tac -> Safe_tac | changeset | files |
| Mon, 29 Sep 1997 11:31:13 +0200 | paulson | Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt | changeset | files |
| Mon, 29 Sep 1997 11:28:23 +0200 | paulson | Safe_tac; qed_spec_mp in FOL | changeset | files |
| Fri, 26 Sep 1997 10:21:14 +0200 | paulson | Minor tidying to use Clarify_tac, etc. | changeset | files |
| Fri, 26 Sep 1997 10:12:04 +0200 | wenzelm | eliminated rules; | changeset | files |
| Thu, 25 Sep 1997 13:25:50 +0200 | paulson | Clarify_tac and some textual improvements | changeset | files |
| Thu, 25 Sep 1997 13:23:41 +0200 | paulson | Clarify_tac; general reorganization | changeset | files |
| Thu, 25 Sep 1997 12:32:14 +0200 | paulson | Deleted obsolete version of clarify_tac | changeset | files |
| Thu, 25 Sep 1997 12:25:29 +0200 | paulson | Deleted the unused list_mk_disj | changeset | files |
| Thu, 25 Sep 1997 12:24:53 +0200 | paulson | Deleted the unused gtake and recoded enumerate to use foldl | changeset | files |
| Thu, 25 Sep 1997 12:20:24 +0200 | paulson | Deleted an obsolete step in TrustServerFinished | changeset | files |
| Thu, 25 Sep 1997 12:19:41 +0200 | paulson | Deleted obsolete axioms inj_serverK and isSym_serverK | changeset | files |
| Thu, 25 Sep 1997 12:14:41 +0200 | paulson | Tidied proofs, using Clarify_tac | changeset | files |
| Thu, 25 Sep 1997 12:13:18 +0200 | paulson | Changed some proofs to use Clarify_tac | changeset | files |
| Thu, 25 Sep 1997 12:10:07 +0200 | paulson | Prints warnings using the "warning" function instead of "writeln" | changeset | files |
| Thu, 25 Sep 1997 12:09:41 +0200 | paulson | Generalized and exported biresolution_from_nets_tac to allow the declaration | changeset | files |
| Thu, 25 Sep 1997 12:08:08 +0200 | paulson | Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac | changeset | files |
| Wed, 24 Sep 1997 12:27:53 +0200 | paulson | sessionK now indexed by nat instead of bool. | changeset | files |
| Wed, 24 Sep 1997 12:26:14 +0200 | paulson | Tidied some proofs using clarify_tac | changeset | files |
| Wed, 24 Sep 1997 12:25:32 +0200 | paulson | clarify_tac and a new simprule | changeset | files |
| Wed, 24 Sep 1997 12:24:41 +0200 | paulson | Names and saves the theorem parts_spies_subset_used | changeset | files |
| Wed, 24 Sep 1997 10:51:52 +0200 | wenzelm | pure_trfuns: added constraint; | changeset | files |
| Tue, 23 Sep 1997 17:35:07 +0200 | wenzelm | added handle_error: ('a -> 'b) -> 'a -> 'b error; | changeset | files |
| Tue, 23 Sep 1997 08:44:57 +0200 | wenzelm | index.html obsolete; | changeset | files |
| Mon, 22 Sep 1997 17:38:55 +0200 | wenzelm | Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; | changeset | files |
| Mon, 22 Sep 1997 17:37:48 +0200 | wenzelm | acks; | changeset | files |
| Mon, 22 Sep 1997 17:37:24 +0200 | wenzelm | added Cambridge fs; | changeset | files |
| Mon, 22 Sep 1997 17:37:03 +0200 | wenzelm | fixed pttrn syntax; | changeset | files |
| Mon, 22 Sep 1997 17:35:52 +0200 | wenzelm | fixed LAM <x,y,zs>.b syntax (may break some unusual cases); | changeset | files |
| Mon, 22 Sep 1997 17:31:57 +0200 | wenzelm | tuned pattern syntax; | changeset | files |
| Mon, 22 Sep 1997 17:31:28 +0200 | wenzelm | tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts | changeset | files |
| Mon, 22 Sep 1997 17:29:42 +0200 | wenzelm | fixed idt/idts vs. pttrn/pttrns; | changeset | files |
| Mon, 22 Sep 1997 16:08:45 +0200 | paulson | Added Cambridge font server | changeset | files |
| Mon, 22 Sep 1997 14:46:56 +0200 | wenzelm | obsolete; | changeset | files |
| Mon, 22 Sep 1997 13:17:29 +0200 | paulson | Simplified SpyKeys to use sessionK instead of clientK and serverK | changeset | files |
| Fri, 19 Sep 1997 18:27:31 +0200 | paulson | First working version with Oops event for session keys | changeset | files |
| Fri, 19 Sep 1997 16:12:21 +0200 | paulson | Full version of TLS including session resumption, but no Oops | changeset | files |
| Fri, 19 Sep 1997 16:11:24 +0200 | paulson | Deleted the obsolete theorem analz_UN1_synth | changeset | files |
| Thu, 18 Sep 1997 13:24:04 +0200 | paulson | Global change: lost->bad and sees Spy->spies | changeset | files |
| Wed, 17 Sep 1997 16:40:52 +0200 | paulson | Deleted the redundant identifier Says_imp_sees_Spy' | changeset | files |
| Wed, 17 Sep 1997 16:39:43 +0200 | paulson | New proof of respond_Spy_not_see_session_key | changeset | files |
| Wed, 17 Sep 1997 16:38:34 +0200 | paulson | Removed the simprule imp_disjL from the analz_image_..._ss to boost speed | changeset | files |
| Wed, 17 Sep 1997 16:37:40 +0200 | paulson | Fixed comments | changeset | files |
| Wed, 17 Sep 1997 16:37:27 +0200 | paulson | Spy can see Notes of the compromised agents | changeset | files |
| Wed, 17 Sep 1997 16:37:21 +0200 | paulson | Now with the sessionK constant and new events ClientAccepts and ServerAccepts | changeset | files |
| Tue, 16 Sep 1997 14:40:01 +0200 | paulson | Addition of SessionIDs to the Hello and Finished messages | changeset | files |
| Tue, 16 Sep 1997 14:04:10 +0200 | paulson | Deleted the redundant simprule not_parts_not_analz | changeset | files |
| Tue, 16 Sep 1997 13:58:02 +0200 | paulson | Deleted the redundant simprule not_parts_not_analz | changeset | files |
| Tue, 16 Sep 1997 13:54:41 +0200 | paulson | Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification | changeset | files |
| Tue, 16 Sep 1997 13:32:22 +0200 | paulson | TLS now with a distinction between premaster secret and master secret | changeset | files |
| Fri, 12 Sep 1997 10:45:51 +0200 | mueller | extended adm_tac; | changeset | files |
| Thu, 11 Sep 1997 16:20:56 +0200 | wenzelm | replaced print_goals_ref hook by print_current_goals_fn and | changeset | files |
| Thu, 11 Sep 1997 16:16:03 +0200 | wenzelm | removed print_goals_ref (which was broken anyway); | changeset | files |
| Thu, 11 Sep 1997 12:24:28 +0200 | paulson | Split base cases from "msg" to "atomic" in order | changeset | files |
| Thu, 11 Sep 1997 12:22:31 +0200 | paulson | Now uses the generic induct_tac | changeset | files |
| Thu, 11 Sep 1997 12:21:34 +0200 | paulson | auto update | changeset | files |
| Wed, 10 Sep 1997 14:18:12 +0200 | nipkow | Added Larry's test for preventing a datatype shadowing a theory. | changeset | files |