| Mon, 10 May 1999 15:26:30 +0200 | wenzelm | pdf setup; | changeset | files |
| Mon, 10 May 1999 15:17:14 +0200 | wenzelm | fixed URLs; | changeset | files |
| Mon, 10 May 1999 15:16:49 +0200 | wenzelm | pdf setup; | changeset | files |
| Fri, 07 May 1999 17:50:43 +0200 | wenzelm | replaced png by pdf; | changeset | files |
| Fri, 07 May 1999 17:49:32 +0200 | wenzelm | pdf pics; | changeset | files |
| Fri, 07 May 1999 11:02:00 +0200 | paulson | tidied | changeset | files |
| Fri, 07 May 1999 10:50:28 +0200 | paulson | tidied | changeset | files |
| Fri, 07 May 1999 10:48:56 +0200 | paulson | new refererences for Inductive manual, but still incomplete | changeset | files |
| Thu, 06 May 1999 19:04:44 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 06 May 1999 19:04:20 +0200 | wenzelm | pdf setup; | changeset | files |
| Thu, 06 May 1999 18:48:46 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Thu, 06 May 1999 18:46:50 +0200 | wenzelm | pdf setup; | changeset | files |
| Thu, 06 May 1999 15:34:36 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 06 May 1999 11:48:26 +0200 | nipkow | More refs. | changeset | files |
| Thu, 06 May 1999 11:48:09 +0200 | nipkow | Refs. | changeset | files |
| Thu, 06 May 1999 11:13:01 +0200 | nipkow | New title page. | changeset | files |
| Wed, 05 May 1999 18:48:32 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 05 May 1999 18:48:02 +0200 | wenzelm | manual.bib; | changeset | files |
| Wed, 05 May 1999 18:47:37 +0200 | wenzelm | no rail; | changeset | files |
| Wed, 05 May 1999 18:41:31 +0200 | wenzelm | fixed FILES; | changeset | files |
| Wed, 05 May 1999 18:35:41 +0200 | wenzelm | improved Makefile; | changeset | files |
| Wed, 05 May 1999 18:26:10 +0200 | wenzelm | improved Makefile; | changeset | files |
| Wed, 05 May 1999 18:24:57 +0200 | wenzelm | isabelle.eps; | changeset | files |
| Wed, 05 May 1999 18:19:03 +0200 | wenzelm | improved Makefile; | changeset | files |
| Wed, 05 May 1999 18:16:03 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 05 May 1999 18:13:56 +0200 | wenzelm | improved Makefile; | changeset | files |
| Wed, 05 May 1999 18:08:01 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Wed, 05 May 1999 18:07:38 +0200 | wenzelm | Common part for Doc Makefiles; | changeset | files |
| Wed, 05 May 1999 16:44:42 +0200 | paulson | Now uses manual.bib; some references updated | changeset | files |
| Wed, 05 May 1999 14:31:31 +0200 | wenzelm | tuned rpm file names; | changeset | files |
| Wed, 05 May 1999 14:31:17 +0200 | wenzelm | updated docs; | changeset | files |
| Wed, 05 May 1999 09:44:48 +0200 | nipkow | Bibtex database for documentation. | changeset | files |
| Wed, 05 May 1999 09:43:53 +0200 | nipkow | Bibtex stuff. | changeset | files |
| Tue, 04 May 1999 19:08:58 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Tue, 04 May 1999 18:56:43 +0200 | wenzelm | HOL; | changeset | files |
| Tue, 04 May 1999 18:55:43 +0200 | wenzelm | removed HOL.tex; | changeset | files |
| Tue, 04 May 1999 18:27:36 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 04 May 1999 18:11:35 +0200 | wenzelm | updated; | changeset | files |
| Tue, 04 May 1999 18:05:34 +0200 | wenzelm | HOL part moved to 'logics-HOL' manual; | changeset | files |
| Tue, 04 May 1999 18:04:45 +0200 | wenzelm | fixed; | changeset | files |
| Tue, 04 May 1999 18:03:56 +0200 | wenzelm | used to be part of 'logics' manual; | changeset | files |
| Tue, 04 May 1999 17:59:55 +0200 | wenzelm | isabelle_zf image; | changeset | files |
| Tue, 04 May 1999 17:59:31 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Tue, 04 May 1999 16:49:24 +0200 | nipkow | Arithmetic. | changeset | files |
| Tue, 04 May 1999 16:18:16 +0200 | wenzelm | add_recdef: removed names / attributes; | changeset | files |
| Tue, 04 May 1999 13:47:28 +0200 | paulson | new definitions of Co and LeadsTo | changeset | files |
| Tue, 04 May 1999 13:32:53 +0200 | wenzelm | transaction: Theory.copy; | changeset | files |
| Tue, 04 May 1999 13:32:35 +0200 | wenzelm | hide prep_ext, merge_theories; | changeset | files |
| Tue, 04 May 1999 11:31:29 +0200 | wenzelm | oops; | changeset | files |
| Tue, 04 May 1999 11:27:25 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 04 May 1999 10:26:00 +0200 | paulson | Invariant -> Always and other tidying | changeset | files |
| Mon, 03 May 1999 19:03:35 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 03 May 1999 18:35:48 +0200 | wenzelm | theory loader stuff updated and improved; | changeset | files |
| Mon, 03 May 1999 14:43:52 +0200 | wenzelm | fixed reqs? | changeset | files |
| Mon, 03 May 1999 11:19:08 +0200 | paulson | improved error handling | changeset | files |
| Mon, 03 May 1999 11:18:44 +0200 | paulson | renamed state variables | changeset | files |
| Mon, 03 May 1999 11:18:11 +0200 | paulson | tidied | changeset | files |
| Mon, 03 May 1999 10:57:14 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 03 May 1999 10:51:44 +0200 | wenzelm | prefer /bin for ./configure; | changeset | files |
| Mon, 03 May 1999 10:47:32 +0200 | wenzelm | try chown root:root; | changeset | files |
| Sat, 01 May 1999 00:10:05 +0200 | wenzelm | renamed 'dummy' to 'dummy_pattern' (less dangerous); | changeset | files |
| Fri, 30 Apr 1999 18:25:10 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 30 Apr 1999 18:13:55 +0200 | wenzelm | method = meth3 (again); | changeset | files |
| Fri, 30 Apr 1999 18:10:35 +0200 | wenzelm | peoper defer_recdef interface; | changeset | files |
| Fri, 30 Apr 1999 18:10:03 +0200 | wenzelm | theory data: copy; | changeset | files |
| Fri, 30 Apr 1999 18:09:33 +0200 | wenzelm | separated recdef / defer_recdef; | changeset | files |
| Fri, 30 Apr 1999 18:08:58 +0200 | wenzelm | tuned defer_recdef interfaces; | changeset | files |
| Fri, 30 Apr 1999 18:07:19 +0200 | wenzelm | comment, interest; | changeset | files |
| Fri, 30 Apr 1999 18:06:49 +0200 | wenzelm | Comment.text; | changeset | files |
| Fri, 30 Apr 1999 18:06:35 +0200 | wenzelm | comment sections; | changeset | files |
| Fri, 30 Apr 1999 18:05:55 +0200 | wenzelm | dummy patterns; | changeset | files |
| Fri, 30 Apr 1999 18:04:42 +0200 | wenzelm | added Isar/comment.ML; | changeset | files |
| Fri, 30 Apr 1999 18:02:16 +0200 | wenzelm | val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term; | changeset | files |
| Fri, 30 Apr 1999 18:01:55 +0200 | wenzelm | theory data: copy; | changeset | files |
| Fri, 30 Apr 1999 18:01:11 +0200 | wenzelm | theory data: copy; | changeset | files |
| Fri, 30 Apr 1999 17:59:36 +0200 | wenzelm | improved icons; | changeset | files |
| Fri, 30 Apr 1999 17:46:14 +0200 | wenzelm | Isabelle icons; | changeset | files |
| Fri, 30 Apr 1999 16:41:10 +0200 | wenzelm | patched sum_case; | changeset | files |
| Thu, 29 Apr 1999 22:45:19 +0200 | berghofe | Obsolete because JDK 1.1.x contains a class ScrollPane | changeset | files |
| Thu, 29 Apr 1999 22:42:38 +0200 | berghofe | Updated to JDK 1.1.x | changeset | files |
| Thu, 29 Apr 1999 18:34:30 +0200 | nipkow | Proof mods due to eta contraction during rewriting. | changeset | files |
| Thu, 29 Apr 1999 18:33:31 +0200 | nipkow | Eta contraction is now performed all the time during rewriting. | changeset | files |
| Thu, 29 Apr 1999 15:35:40 +0200 | wenzelm | currently disabled; | changeset | files |
| Thu, 29 Apr 1999 15:34:43 +0200 | wenzelm | *** empty log message *** | changeset | files |
| Thu, 29 Apr 1999 10:51:58 +0200 | paulson | made many specification operators infix | changeset | files |
| Wed, 28 Apr 1999 13:36:31 +0200 | paulson | eliminated theory UNITY/Traces | changeset | files |
| Tue, 27 Apr 1999 15:39:43 +0200 | wenzelm | improper simp methods; | changeset | files |
| Tue, 27 Apr 1999 15:32:37 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 27 Apr 1999 15:14:44 +0200 | wenzelm | fold / unfold methods; | changeset | files |
| Tue, 27 Apr 1999 15:14:22 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 27 Apr 1999 15:13:58 +0200 | wenzelm | no Toplevel.print for by, ., ..; | changeset | files |
| Tue, 27 Apr 1999 15:13:35 +0200 | wenzelm | improved print_state; | changeset | files |
| Tue, 27 Apr 1999 15:13:18 +0200 | wenzelm | verbose flag; | changeset | files |
| Tue, 27 Apr 1999 15:12:34 +0200 | wenzelm | use_thy_only made pervasive; | changeset | files |
| Tue, 27 Apr 1999 15:10:36 +0200 | wenzelm | added Isar_examples/NatSum.thy; | changeset | files |
| Tue, 27 Apr 1999 13:05:52 +0200 | nipkow | Old stuff. | changeset | files |
| Tue, 27 Apr 1999 10:52:25 +0200 | wenzelm | proper quiet_mode; | changeset | files |
| Tue, 27 Apr 1999 10:51:16 +0200 | wenzelm | adapted add_inductive, add_record; | changeset | files |
| Tue, 27 Apr 1999 10:50:50 +0200 | wenzelm | adapted add_inductive; | changeset | files |
| Tue, 27 Apr 1999 10:50:31 +0200 | wenzelm | intrs attributes; | changeset | files |
| Tue, 27 Apr 1999 10:50:08 +0200 | wenzelm | proper quiet_mode; | changeset | files |
| Tue, 27 Apr 1999 10:49:52 +0200 | wenzelm | iff_add_global (from simpdata.ML); | changeset | files |
| Tue, 27 Apr 1999 10:47:40 +0200 | wenzelm | support forward chaining; | changeset | files |
| Tue, 27 Apr 1999 10:46:37 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 27 Apr 1999 10:45:20 +0200 | wenzelm | added Isar_examples/Cantor.ML; | changeset | files |
| Tue, 27 Apr 1999 10:44:42 +0200 | wenzelm | hol_setup, simpdata_setup; | changeset | files |
| Tue, 27 Apr 1999 10:44:17 +0200 | wenzelm | "iff" attribute; | changeset | files |
| Tue, 27 Apr 1999 10:43:52 +0200 | wenzelm | hol_setup; | changeset | files |
| Tue, 27 Apr 1999 10:42:55 +0200 | wenzelm | "!" made keyword; | changeset | files |
| Tue, 27 Apr 1999 10:42:37 +0200 | wenzelm | opt_thm_name: name optional; | changeset | files |
| Tue, 27 Apr 1999 10:42:08 +0200 | wenzelm | added oooo; | changeset | files |
| Mon, 26 Apr 1999 13:25:49 +0200 | paulson | fixed a bug many years old in rule plusEC | changeset | files |
| Mon, 26 Apr 1999 10:44:45 +0200 | wenzelm | tuned msgs; | changeset | files |
| Fri, 23 Apr 1999 17:47:47 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 23 Apr 1999 17:34:47 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 23 Apr 1999 17:02:10 +0200 | wenzelm | elaborated; | changeset | files |
| Fri, 23 Apr 1999 17:01:50 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 23 Apr 1999 17:01:36 +0200 | wenzelm | tuned antiquotations; | changeset | files |
| Fri, 23 Apr 1999 16:38:22 +0200 | wenzelm | improved 'single' method; | changeset | files |
| Fri, 23 Apr 1999 16:33:23 +0200 | wenzelm | added thus, hence; | changeset | files |
| Fri, 23 Apr 1999 16:33:03 +0200 | wenzelm | added FINISHED, same_tac; | changeset | files |
| Fri, 23 Apr 1999 16:31:12 +0200 | wenzelm | use /usr/share and /usr/bin; | changeset | files |
| Fri, 23 Apr 1999 12:23:21 +0200 | paulson | Now for recdefs that omit the WF relation; | changeset | files |
| Fri, 23 Apr 1999 12:22:30 +0200 | paulson | Now for recdefs that omit the WF relation | changeset | files |
| Fri, 23 Apr 1999 12:20:22 +0200 | paulson | Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml | changeset | files |
| Fri, 23 Apr 1999 11:51:38 +0200 | wenzelm | chgrp isabelle; | changeset | files |
| Fri, 23 Apr 1999 11:50:35 +0200 | wenzelm | detailed proofs; | changeset | files |
| Fri, 23 Apr 1999 11:50:17 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 23 Apr 1999 11:48:37 +0200 | wenzelm | oops; | changeset | files |
| Thu, 22 Apr 1999 18:25:24 +0200 | wenzelm | fixed IO; | changeset | files |
| Thu, 22 Apr 1999 18:25:07 +0200 | wenzelm | improved load paths; | changeset | files |
| Thu, 22 Apr 1999 18:23:45 +0200 | wenzelm | single method: include not_elim, imp_elim; | changeset | files |
| Thu, 22 Apr 1999 18:20:37 +0200 | wenzelm | more graceful handling of load paths; | changeset | files |
| Thu, 22 Apr 1999 18:18:47 +0200 | wenzelm | improved auto dir handling; | changeset | files |
| Thu, 22 Apr 1999 15:16:59 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 22 Apr 1999 15:03:50 +0200 | wenzelm | make Isabelle rpm packages for Linux/x86 from the distribution; | changeset | files |
| Thu, 22 Apr 1999 13:28:11 +0200 | wenzelm | use_thy etc.: may specify path prefix, which is temporarily used as load path; | changeset | files |
| Thu, 22 Apr 1999 13:16:22 +0200 | wenzelm | switch_theory: Context.pass; | changeset | files |
| Thu, 22 Apr 1999 13:04:50 +0200 | wenzelm | recdef (TFL) now requires theory Recdef; | changeset | files |
| Thu, 22 Apr 1999 13:04:23 +0200 | wenzelm | recdef requires theory Recdef; | changeset | files |
| Thu, 22 Apr 1999 13:03:46 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 22 Apr 1999 13:03:10 +0200 | wenzelm | rep_datatype syntax: 'induction' instead of 'induct'; | changeset | files |
| Thu, 22 Apr 1999 12:50:39 +0200 | wenzelm | add_recdef: actual simpset; | changeset | files |
| Thu, 22 Apr 1999 12:49:34 +0200 | wenzelm | recdef adapted to RecdefPackage.add_recdef; | changeset | files |
| Thu, 22 Apr 1999 12:49:00 +0200 | wenzelm | Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML; | changeset | files |
| Thu, 22 Apr 1999 12:47:13 +0200 | mueller | added ex and Modelcheck | changeset | files |
| Thu, 22 Apr 1999 12:47:07 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 22 Apr 1999 12:42:14 +0200 | mueller | added for mucke translation; | changeset | files |
| Thu, 22 Apr 1999 12:40:11 +0200 | mueller | deleted some old examples in Modelcheck; | changeset | files |
| Thu, 22 Apr 1999 11:09:05 +0200 | mueller | added translation from IOA to mucalculus and corresponding modelchecker examples; | changeset | files |
| Thu, 22 Apr 1999 11:06:35 +0200 | mueller | moved this trivial example to new ex dir; | changeset | files |
| Thu, 22 Apr 1999 11:05:48 +0200 | mueller | changed to include new subdirs ex and Modelcheck; | changeset | files |
| Thu, 22 Apr 1999 11:02:46 +0200 | mueller | put types into "" because of signature clash; | changeset | files |
| Thu, 22 Apr 1999 11:00:30 +0200 | mueller | added frontend syntax for IOA, moved trivial examples to folder ex; | changeset | files |
| Thu, 22 Apr 1999 10:56:37 +0200 | mueller | added modelchecker mucke besides modelchecker eindhoven; | changeset | files |
| Thu, 22 Apr 1999 10:55:23 +0200 | mueller | delete old files for adding second modelchecker connection; | changeset | files |
| Wed, 21 Apr 1999 19:03:11 +0200 | wenzelm | $ML_HOME/.arch-n-opsys 2>/dev/null; | changeset | files |
| Wed, 21 Apr 1999 18:50:35 +0200 | wenzelm | smlnj-110 setup made default; | changeset | files |
| Wed, 21 Apr 1999 18:46:58 +0200 | wenzelm | /usr/share/smlnj/bin; | changeset | files |
| Wed, 21 Apr 1999 17:11:34 +0200 | wenzelm | Isamode 2.6 requires patch; | changeset | files |
| Wed, 21 Apr 1999 16:30:35 +0200 | wenzelm | added is_current; | changeset | files |
| Tue, 20 Apr 1999 15:23:43 +0200 | wenzelm | fixed ISABELLE_HOME/lib/logo/isabelle-tiny.xpm; | changeset | files |
| Tue, 20 Apr 1999 15:20:27 +0200 | wenzelm | temporarily fake quiet_mode; | changeset | files |
| Tue, 20 Apr 1999 15:19:52 +0200 | wenzelm | temporarily reverted to 1.24; | changeset | files |
| Tue, 20 Apr 1999 14:38:17 +0200 | paulson | IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly) | changeset | files |
| Tue, 20 Apr 1999 14:36:19 +0200 | paulson | Main is the correct parent | changeset | files |
| Tue, 20 Apr 1999 14:35:12 +0200 | paulson | new result extend_LeadsTo | changeset | files |
| Tue, 20 Apr 1999 14:34:47 +0200 | paulson | should not refer to Datatype | changeset | files |
| Tue, 20 Apr 1999 14:33:48 +0200 | paulson | addition of Kerberos IV example | changeset | files |
| Tue, 20 Apr 1999 14:32:48 +0200 | paulson | tidied | changeset | files |
| Mon, 19 Apr 1999 17:53:38 +0200 | wenzelm | improved usage; | changeset | files |
| Fri, 16 Apr 1999 18:52:03 +0200 | wenzelm | loadpath replaced; | changeset | files |
| Fri, 16 Apr 1999 17:48:46 +0200 | wenzelm | and_list; | changeset | files |
| Fri, 16 Apr 1999 17:48:31 +0200 | wenzelm | lifted enum; | changeset | files |
| Fri, 16 Apr 1999 17:47:06 +0200 | wenzelm | may specify induction predicates as well; | changeset | files |
| Fri, 16 Apr 1999 17:46:02 +0200 | wenzelm | added Isar_examples; | changeset | files |
| Fri, 16 Apr 1999 17:44:29 +0200 | wenzelm | Miscellaneous Isabelle/Isar examples for Higher-Order Logic. | changeset | files |
| Fri, 16 Apr 1999 16:47:30 +0200 | wenzelm | lemmas about proper subset relation; | changeset | files |
| Fri, 16 Apr 1999 14:50:30 +0200 | wenzelm | Proof by induction on types / set / functions. | changeset | files |
| Fri, 16 Apr 1999 14:49:57 +0200 | wenzelm | print_datatypes; | changeset | files |
| Fri, 16 Apr 1999 14:49:34 +0200 | wenzelm | added Tools/induct_method.ML; | changeset | files |
| Fri, 16 Apr 1999 14:49:09 +0200 | wenzelm | 'HOL/recdef' theory data; | changeset | files |
| Fri, 16 Apr 1999 14:49:06 +0200 | wenzelm | 'HOL/recdef' theory data; | changeset | files |
| Fri, 16 Apr 1999 14:48:16 +0200 | wenzelm | 'HOL/inductive' theory data; | changeset | files |
| Fri, 16 Apr 1999 14:43:26 +0200 | wenzelm | Sign.base_name fid; | changeset | files |
| Fri, 16 Apr 1999 14:42:44 +0200 | wenzelm | added incr_indexes, incr_indexes_wrt; | changeset | files |
| Thu, 15 Apr 1999 18:10:49 +0200 | nipkow | Proof mod. | changeset | files |
| Thu, 15 Apr 1999 18:10:37 +0200 | nipkow | Added new thms. | changeset | files |
| Wed, 14 Apr 1999 19:07:39 +0200 | wenzelm | quiet_mode; | changeset | files |
| Wed, 14 Apr 1999 19:07:04 +0200 | wenzelm | Tools/inductive_package.ML; | changeset | files |
| Wed, 14 Apr 1999 19:05:28 +0200 | wenzelm | triple_swap; | changeset | files |
| Wed, 14 Apr 1999 19:05:10 +0200 | wenzelm | Wrapper module for Konrad Slind's TFL package. | changeset | files |
| Wed, 14 Apr 1999 18:55:29 +0200 | wenzelm | remoced old set_current_thy; | changeset | files |
| Wed, 14 Apr 1999 15:58:01 +0200 | wenzelm | tuned messages; | changeset | files |
| Wed, 14 Apr 1999 14:44:04 +0200 | wenzelm | intrs: names and atts; | changeset | files |
| Wed, 14 Apr 1999 14:42:53 +0200 | wenzelm | tuned comments; | changeset | files |
| Wed, 14 Apr 1999 14:42:23 +0200 | wenzelm | tuned comments; | changeset | files |
| Wed, 14 Apr 1999 14:41:01 +0200 | wenzelm | tuned comments; | changeset | files |
| Wed, 14 Apr 1999 14:40:43 +0200 | wenzelm | intrs: provide names and atts; | changeset | files |
| Wed, 14 Apr 1999 11:32:50 +0200 | wenzelm | cleaned comments; | changeset | files |
| Wed, 14 Apr 1999 11:24:09 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 14 Apr 1999 11:17:16 +0200 | wenzelm | fixed named type infixes (actual BUG!); | changeset | files |
| Tue, 13 Apr 1999 12:39:35 +0200 | wenzelm | updated isatool install; | changeset | files |
| Tue, 13 Apr 1999 12:36:11 +0200 | wenzelm | -p option; | changeset | files |
| Tue, 13 Apr 1999 12:35:28 +0200 | wenzelm | adapted isatool install; | changeset | files |
| Tue, 13 Apr 1999 12:35:11 +0200 | wenzelm | improved isatool install; | changeset | files |
| Tue, 13 Apr 1999 10:34:30 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 12 Apr 1999 16:20:04 +0200 | wenzelm | ML_PLATFORM; | changeset | files |
| Mon, 12 Apr 1999 15:52:48 +0200 | wenzelm | ML_PLATFORM; | changeset | files |
| Wed, 07 Apr 1999 15:43:16 +0200 | wenzelm | fixed @@; | changeset | files |
| Sun, 04 Apr 1999 16:07:33 +0200 | paulson | fixed bib file | changeset | files |
| Sat, 03 Apr 1999 13:05:42 +0200 | wenzelm | fixed; | changeset | files |
| Thu, 01 Apr 1999 18:42:48 +0200 | pusch | new definition for nth. | changeset | files |
| Wed, 31 Mar 1999 16:14:20 +0200 | nipkow | useless relic | changeset | files |
| Tue, 30 Mar 1999 13:17:55 +0200 | nipkow | arith_tac | changeset | files |
| Fri, 19 Mar 1999 11:26:40 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 19 Mar 1999 11:24:00 +0100 | wenzelm | common qed and end of proofs; | changeset | files |
| Thu, 18 Mar 1999 16:44:53 +0100 | nipkow | * New bounded quantifier syntax (input only): | changeset | files |
| Thu, 18 Mar 1999 16:42:34 +0100 | nipkow | New bounded quantifier syntax: !x<i. P etc | changeset | files |
| Thu, 18 Mar 1999 11:19:03 +0100 | paulson | added new theory Yahalom_Bad | changeset | files |
| Thu, 18 Mar 1999 10:41:33 +0100 | paulson | added new theory Yahalom_Bad | changeset | files |
| Thu, 18 Mar 1999 10:41:00 +0100 | paulson | exchanged the order of Gets and Notes in datatype event | changeset | files |
| Wed, 17 Mar 1999 18:01:41 +0100 | wenzelm | fixed thm_name again; | changeset | files |
| Wed, 17 Mar 1999 17:20:36 +0100 | wenzelm | Theory.sign_of; | changeset | files |
| Wed, 17 Mar 1999 17:19:18 +0100 | wenzelm | xnum token class; | changeset | files |
| Wed, 17 Mar 1999 17:18:54 +0100 | wenzelm | xstr token class; | changeset | files |
| Wed, 17 Mar 1999 16:53:46 +0100 | wenzelm | Theory.sign_of; | changeset | files |
| Wed, 17 Mar 1999 16:53:32 +0100 | wenzelm | fixed axclass_tac; | changeset | files |
| Wed, 17 Mar 1999 16:45:53 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 17 Mar 1999 16:33:47 +0100 | wenzelm | Theory.sign_of; | changeset | files |
| Wed, 17 Mar 1999 16:33:00 +0100 | wenzelm | qualify Theory.sign_of etc.; | changeset | files |
| Wed, 17 Mar 1999 16:32:38 +0100 | wenzelm | fixed msg; | changeset | files |
| Wed, 17 Mar 1999 15:43:04 +0100 | wenzelm | tuned msg; | changeset | files |
| Wed, 17 Mar 1999 13:56:29 +0100 | wenzelm | axclass_tac lost an argument; | changeset | files |
| Wed, 17 Mar 1999 13:54:42 +0100 | wenzelm | HOL/typedef: fixed type inference for representing set; | changeset | files |
| Wed, 17 Mar 1999 13:50:51 +0100 | wenzelm | rep_datatype: '_i' version, attributes, outer syntax; | changeset | files |
| Wed, 17 Mar 1999 13:49:39 +0100 | wenzelm | local open OuterParse; | changeset | files |
| Wed, 17 Mar 1999 13:49:14 +0100 | wenzelm | actually check non-emptiness theorem; | changeset | files |
| Wed, 17 Mar 1999 13:47:34 +0100 | wenzelm | fixed typedef representing set; | changeset | files |
| Wed, 17 Mar 1999 13:47:04 +0100 | wenzelm | adapted rep_datatype; | changeset | files |
| Wed, 17 Mar 1999 13:46:23 +0100 | wenzelm | added dest_mem; | changeset | files |
| Wed, 17 Mar 1999 13:44:43 +0100 | wenzelm | theory data; | changeset | files |
| Wed, 17 Mar 1999 13:42:42 +0100 | wenzelm | adapted AxClass.add_axclass; | changeset | files |
| Wed, 17 Mar 1999 13:41:50 +0100 | wenzelm | tuned msgs; | changeset | files |
| Wed, 17 Mar 1999 13:41:14 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 17 Mar 1999 13:40:21 +0100 | wenzelm | cleaned comments; | changeset | files |
| Wed, 17 Mar 1999 13:39:44 +0100 | wenzelm | added apply_cond_open; | changeset | files |
| Wed, 17 Mar 1999 13:39:21 +0100 | wenzelm | added (improper_)command; | changeset | files |
| Wed, 17 Mar 1999 13:39:01 +0100 | wenzelm | added simple_arity, spec_name, spec_opt_name; | changeset | files |
| Wed, 17 Mar 1999 13:36:23 +0100 | wenzelm | added '_i' versions; | changeset | files |
| Wed, 17 Mar 1999 13:34:49 +0100 | wenzelm | OuterSyntax.(improper_)command; | changeset | files |
| Wed, 17 Mar 1999 13:33:13 +0100 | wenzelm | added assert_super; | changeset | files |
| Wed, 17 Mar 1999 13:32:20 +0100 | wenzelm | added def_name; | changeset | files |
| Wed, 17 Mar 1999 13:31:19 +0100 | wenzelm | added cond_extern_thm_sg; | changeset | files |
| Wed, 17 Mar 1999 13:30:24 +0100 | wenzelm | AxClass.setup; | changeset | files |
| Wed, 17 Mar 1999 13:30:09 +0100 | wenzelm | axclass.ML loaded after Isar; | changeset | files |
| Fri, 12 Mar 1999 22:02:51 +0100 | wenzelm | made weblint happy; | changeset | files |
| Fri, 12 Mar 1999 18:49:02 +0100 | wenzelm | comment; | changeset | files |
| Fri, 12 Mar 1999 18:48:51 +0100 | wenzelm | removed obsolete user data stuff; | changeset | files |
| Fri, 12 Mar 1999 18:48:11 +0100 | wenzelm | theory: include parent links; | changeset | files |
| Thu, 11 Mar 1999 21:59:26 +0100 | wenzelm | outer syntax for 'datatype'; | changeset | files |
| Thu, 11 Mar 1999 21:58:54 +0100 | wenzelm | add_primrec(_i): attributes; | changeset | files |
| Thu, 11 Mar 1999 21:58:12 +0100 | wenzelm | outer syntax for 'record'; | changeset | files |
| Thu, 11 Mar 1999 21:57:34 +0100 | wenzelm | named witnesses: PureThy.get_thmss; | changeset | files |
| Thu, 11 Mar 1999 21:56:22 +0100 | wenzelm | primrec: empty attributes; | changeset | files |
| Thu, 11 Mar 1999 21:55:23 +0100 | wenzelm | tuned opt_mixfix failure; | changeset | files |
| Thu, 11 Mar 1999 21:53:50 +0100 | wenzelm | add_title; | changeset | files |
| Thu, 11 Mar 1999 21:53:36 +0100 | wenzelm | added 'title'; | changeset | files |
| Thu, 11 Mar 1999 21:52:49 +0100 | wenzelm | tuned space; | changeset | files |
| Thu, 11 Mar 1999 21:52:32 +0100 | wenzelm | comment; | changeset | files |
| Thu, 11 Mar 1999 21:51:49 +0100 | wenzelm | workaround default_name problem; | changeset | files |
| Thu, 11 Mar 1999 13:20:35 +0100 | wenzelm | removed foo_build_completed -- now handled by session management (via usedir); | changeset | files |
| Thu, 11 Mar 1999 12:34:10 +0100 | wenzelm | include 'README'; | changeset | files |
| Thu, 11 Mar 1999 12:33:34 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 11 Mar 1999 12:32:40 +0100 | wenzelm | moved Thy/session.ML to Isar/session.ML; | changeset | files |
| Wed, 10 Mar 1999 17:24:26 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 10 Mar 1999 17:06:35 +0100 | wenzelm | -x option; | changeset | files |
| Wed, 10 Mar 1999 16:31:33 +0100 | wenzelm | updated; | changeset | files |
| Wed, 10 Mar 1999 13:44:55 +0100 | wenzelm | report session path; | changeset | files |
| Wed, 10 Mar 1999 13:17:46 +0100 | wenzelm | report path instead of actual session; | changeset | files |
| Wed, 10 Mar 1999 10:55:12 +0100 | wenzelm | HTML output; | changeset | files |
| Wed, 10 Mar 1999 10:53:53 +0100 | wenzelm | maintain current/parent index; | changeset | files |
| Wed, 10 Mar 1999 10:53:02 +0100 | wenzelm | output: some symbol translations; | changeset | files |
| Wed, 10 Mar 1999 10:47:13 +0100 | wenzelm | parent_session; | changeset | files |
| Wed, 10 Mar 1999 10:43:59 +0100 | paulson | allow meta_outer to do nothing | changeset | files |
| Wed, 10 Mar 1999 10:42:57 +0100 | paulson | updating both Yahalom protocols to the Gets model | changeset | files |
| Wed, 10 Mar 1999 10:42:40 +0100 | paulson | updated not_bad_tac for the Gets model | changeset | files |
| Wed, 10 Mar 1999 10:42:11 +0100 | paulson | deleted obsolete comments | changeset | files |
| Tue, 09 Mar 1999 12:20:22 +0100 | wenzelm | Present.theory_source; | changeset | files |
| Tue, 09 Mar 1999 12:20:04 +0100 | wenzelm | begin/end_theory: presentation; | changeset | files |
| Tue, 09 Mar 1999 12:19:25 +0100 | wenzelm | checkpoint -- basic functionality only; | changeset | files |
| Tue, 09 Mar 1999 12:18:46 +0100 | wenzelm | added use_path; | changeset | files |
| Tue, 09 Mar 1999 12:18:02 +0100 | wenzelm | IsarThy.begin/end_theory; | changeset | files |
| Tue, 09 Mar 1999 12:17:40 +0100 | wenzelm | Present.theorem; | changeset | files |
| Tue, 09 Mar 1999 12:13:58 +0100 | wenzelm | fixed add_path reset; | changeset | files |
| Tue, 09 Mar 1999 12:13:11 +0100 | wenzelm | still fake, passes BrowserInfo; | changeset | files |
| Tue, 09 Mar 1999 12:12:45 +0100 | wenzelm | HTML markup elements. | changeset | files |
| Tue, 09 Mar 1999 12:12:02 +0100 | wenzelm | added html.ML, browser_info.ML; | changeset | files |
| Tue, 09 Mar 1999 12:11:29 +0100 | wenzelm | token translation: real; | changeset | files |
| Tue, 09 Mar 1999 12:11:00 +0100 | wenzelm | added strlen_real, setmp_margin; | changeset | files |
| Tue, 09 Mar 1999 12:10:13 +0100 | wenzelm | tuned using nth_elem_string, exists_string; | changeset | files |
| Tue, 09 Mar 1999 12:09:51 +0100 | wenzelm | added make, dir; | changeset | files |
| Tue, 09 Mar 1999 12:09:22 +0100 | wenzelm | added mkdir; | changeset | files |
| Tue, 09 Mar 1999 12:09:05 +0100 | wenzelm | added Buffer; | changeset | files |
| Tue, 09 Mar 1999 12:08:50 +0100 | wenzelm | simple string buffers; | changeset | files |
| Tue, 09 Mar 1999 12:08:08 +0100 | wenzelm | *** empty log message *** | changeset | files |
| Tue, 09 Mar 1999 12:07:52 +0100 | wenzelm | pretty_thm_no_quote; | changeset | files |
| Tue, 09 Mar 1999 12:07:32 +0100 | wenzelm | HTML.setup; | changeset | files |
| Tue, 09 Mar 1999 12:07:16 +0100 | wenzelm | added nth_elem_string, exists_string; | changeset | files |
| Tue, 09 Mar 1999 12:06:09 +0100 | wenzelm | token translation: real; | changeset | files |
| Tue, 09 Mar 1999 12:05:07 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 09 Mar 1999 11:09:01 +0100 | paulson | tidied | changeset | files |
| Tue, 09 Mar 1999 11:01:39 +0100 | paulson | Added Bella's "Gets" model for Otway_Rees. Also affects some other theories. | changeset | files |
| Mon, 08 Mar 1999 13:49:53 +0100 | nipkow | Suc -> +1 | changeset | files |
| Mon, 08 Mar 1999 13:49:14 +0100 | nipkow | modified zip | changeset | files |
| Fri, 05 Mar 1999 12:11:54 +0100 | berghofe | Fixed bug in add_datatype_axm: | changeset | files |
| Thu, 04 Mar 1999 14:23:51 +0100 | wenzelm | fixed again; | changeset | files |
| Wed, 03 Mar 1999 11:27:10 +0100 | paulson | expandshort | changeset | files |
| Wed, 03 Mar 1999 11:26:36 +0100 | paulson | added UNITY/Extend | changeset | files |
| Wed, 03 Mar 1999 11:15:18 +0100 | paulson | expandshort | changeset | files |
| Wed, 03 Mar 1999 11:12:29 +0100 | paulson | tidied | changeset | files |
| Wed, 03 Mar 1999 10:50:42 +0100 | paulson | UNITY fully working at last... | changeset | files |
| Wed, 03 Mar 1999 10:36:24 +0100 | paulson | expandshort | changeset | files |
| Wed, 03 Mar 1999 10:32:35 +0100 | paulson | new theory of extending the state space | changeset | files |
| Mon, 01 Mar 1999 19:10:43 +0100 | wenzelm | fixed {ISABELLE}; | changeset | files |
| Mon, 01 Mar 1999 18:38:43 +0100 | paulson | removed the infernal States, eqStates, compatible, etc. | changeset | files |
| Mon, 01 Mar 1999 18:37:52 +0100 | paulson | tidied | changeset | files |
| Mon, 01 Mar 1999 18:37:23 +0100 | paulson | simpler proofs of congruence rules | changeset | files |
| Mon, 01 Mar 1999 18:11:54 +0100 | paulson | new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq | changeset | files |
| Mon, 01 Mar 1999 15:57:29 +0100 | paulson | simpler proofs of congruence rules | changeset | files |
| Mon, 22 Feb 1999 10:21:59 +0100 | paulson | new image laws | changeset | files |
| Mon, 22 Feb 1999 10:20:25 +0100 | paulson | added a commment on the "ext" rule | changeset | files |
| Mon, 22 Feb 1999 10:19:32 +0100 | paulson | new theorems Pow_0 and Pow_insert; renamed other Pow theorems | changeset | files |
| Mon, 22 Feb 1999 10:16:59 +0100 | paulson | added rev_bexI | changeset | files |
| Thu, 18 Feb 1999 12:15:55 +0100 | wenzelm | fixed order of multiple -m options; | changeset | files |
| Thu, 18 Feb 1999 12:05:16 +0100 | grobauer | fixed geometry; | changeset | files |
| Tue, 16 Feb 1999 10:54:55 +0100 | paulson | tidying in conjuntion with the TISSEC paper; replaced (unit option) | changeset | files |
| Tue, 16 Feb 1999 10:50:35 +0100 | paulson | new theorem image_Union_eq | changeset | files |
| Sat, 13 Feb 1999 22:08:54 +0100 | wenzelm | foldl_string; | changeset | files |
| Fri, 12 Feb 1999 14:40:56 +0100 | oheimb | renamed space2 to spacespace | changeset | files |
| Fri, 12 Feb 1999 13:56:21 +0100 | wenzelm | tuned pretty format lookup; | changeset | files |
| Fri, 12 Feb 1999 13:55:54 +0100 | wenzelm | pretty_thm: quote terms (separately); | changeset | files |
| Thu, 11 Feb 1999 21:25:21 +0100 | wenzelm | Symbol.output subject to print mode; | changeset | files |
| Thu, 11 Feb 1999 21:19:56 +0100 | wenzelm | -m isabelle_font; | changeset | files |
| Thu, 11 Feb 1999 21:18:56 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 11 Feb 1999 21:18:35 +0100 | wenzelm | Present.init; | changeset | files |
| Thu, 11 Feb 1999 21:18:19 +0100 | wenzelm | init, finish; | changeset | files |
| Thu, 11 Feb 1999 21:17:10 +0100 | wenzelm | proper handling of print_mode wrt. Pretty.sym; | changeset | files |
| Thu, 11 Feb 1999 21:16:30 +0100 | wenzelm | added output_width; | changeset | files |
| Thu, 11 Feb 1999 21:15:46 +0100 | wenzelm | sym: Symbol.output_width; | changeset | files |
| Thu, 11 Feb 1999 21:15:27 +0100 | wenzelm | val appends: T list -> T; | changeset | files |
| Thu, 11 Feb 1999 15:30:10 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 09 Feb 1999 10:47:21 +0100 | paulson | tidied; better error messages | changeset | files |
| Tue, 09 Feb 1999 10:45:55 +0100 | paulson | new lemma surjD | changeset | files |
| Mon, 08 Feb 1999 17:33:47 +0100 | wenzelm | Context.fetch, Context.setmp; | changeset | files |
| Mon, 08 Feb 1999 17:33:24 +0100 | wenzelm | "files" keyword! | changeset | files |
| Mon, 08 Feb 1999 17:33:03 +0100 | wenzelm | use: provide context; | changeset | files |
| Mon, 08 Feb 1999 17:32:24 +0100 | wenzelm | tuned msgs; | changeset | files |
| Mon, 08 Feb 1999 17:32:06 +0100 | wenzelm | tuned msg; | changeset | files |
| Mon, 08 Feb 1999 17:31:50 +0100 | wenzelm | added fetch, fetch_theory; | changeset | files |
| Mon, 08 Feb 1999 17:30:22 +0100 | wenzelm | ~~; | changeset | files |
| Mon, 08 Feb 1999 17:29:08 +0100 | wenzelm | path element specification '~~' refers to '$ISABELLE_HOME'; | changeset | files |
| Mon, 08 Feb 1999 15:55:35 +0100 | wenzelm | no deps on compile time sources; | changeset | files |
| Mon, 08 Feb 1999 15:54:44 +0100 | wenzelm | isatool logo; | changeset | files |
| Mon, 08 Feb 1999 15:53:56 +0100 | wenzelm | -i option; | changeset | files |
| Mon, 08 Feb 1999 13:02:56 +0100 | wenzelm | updated (Stephan Merz); | changeset | files |
| Mon, 08 Feb 1999 13:02:42 +0100 | wenzelm | updated TLA; | changeset | files |
| Fri, 05 Feb 1999 21:26:20 +0100 | wenzelm | made MLWorks happy; | changeset | files |
| Fri, 05 Feb 1999 21:14:17 +0100 | wenzelm | examples made separate dirs; | changeset | files |
| Fri, 05 Feb 1999 21:12:45 +0100 | wenzelm | add_path; | changeset | files |
| Fri, 05 Feb 1999 21:12:18 +0100 | wenzelm | Hyperreal made part of Real; | changeset | files |
| Fri, 05 Feb 1999 21:11:41 +0100 | wenzelm | Session.use_dir: check parent; | changeset | files |
| Fri, 05 Feb 1999 21:10:19 +0100 | wenzelm | *** empty log message *** | changeset | files |
| Fri, 05 Feb 1999 21:06:24 +0100 | wenzelm | more robust handling of theory context; | changeset | files |
| Fri, 05 Feb 1999 21:04:58 +0100 | wenzelm | improved theory, context, update_context; | changeset | files |
| Fri, 05 Feb 1999 21:04:31 +0100 | wenzelm | improved 'theory'; | changeset | files |
| Fri, 05 Feb 1999 21:03:33 +0100 | wenzelm | improved msg; | changeset | files |
| Fri, 05 Feb 1999 21:03:06 +0100 | wenzelm | use_thy, update_thy: Context.save; | changeset | files |
| Fri, 05 Feb 1999 21:02:17 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 05 Feb 1999 21:01:53 +0100 | wenzelm | time_use made pervasive; | changeset | files |
| Fri, 05 Feb 1999 20:58:17 +0100 | wenzelm | use_dir: check parent, more robust exit; | changeset | files |
| Fri, 05 Feb 1999 20:57:37 +0100 | wenzelm | more robust RC; | changeset | files |
| Fri, 05 Feb 1999 20:57:18 +0100 | wenzelm | setmp: theory option; | changeset | files |
| Fri, 05 Feb 1999 20:56:50 +0100 | wenzelm | Session.finish (); | changeset | files |