Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
renamed Comment.empty to Comment.none;
1999-05-25, by wenzelm
renamed Comment.empty to Comment.none;
1999-05-25, by wenzelm
renamed empty to none;
1999-05-25, by wenzelm
fixed cvs Id;
1999-05-25, by wenzelm
outer syntax keyword classification;
1999-05-24, by wenzelm
added keyword classification;
1999-05-24, by wenzelm
tuned print_context;
1999-05-24, by wenzelm
write_keywords generates outer syntax keyword classification in elisp;
1999-05-24, by wenzelm
outer syntax keyword classification;
1999-05-24, by wenzelm
renamed Lprg to Lift; simplified proof of Always_nonneg
1999-05-24, by paulson
int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
1999-05-24, by paulson
Better simplification of (nat #0), (int (Suc 0)), etc
1999-05-24, by paulson
UN_singleton->UN_constant_eq removes clash with other UN_singleton
1999-05-24, by paulson
new rule single_leadsTo_I; stronger PSP rule
1999-05-24, by paulson
increasing makes sense only for partial orderings
1999-05-24, by paulson
generalized increasing_size to mono_increasing_o
1999-05-24, by paulson
updated for stronger version of psp
1999-05-24, by paulson
new rule single_LeadsTo_I; stronger PSP rule; PSP_stable2->PSP_Stable2
1999-05-24, by paulson
expandshort
1999-05-24, by paulson
lists are partially ordered by the prefix relation
1999-05-24, by paulson
using generic rules when possible
1999-05-24, by paulson
Theory of the "Follows" relation
1999-05-24, by paulson
Increasing makes sense only for partial orderings
1999-05-24, by paulson
generalized Increasing_size to mono_Increasing_o
1999-05-24, by paulson
tidied
1999-05-24, by paulson
renamed PSP_stable2->PSP_Stable2
1999-05-24, by paulson
now uses mono_Increasing_o
1999-05-24, by paulson
updated for stronger version of psp
1999-05-24, by paulson
Configuration for ProofGeneral of LFCS Edinburgh.
1999-05-21, by wenzelm
Configuration for David Aspinall's Isamode.
1999-05-21, by wenzelm
Miscellaneous interfaces.
1999-05-21, by wenzelm
Isamode.setup, ProofGeneral.setup;
1999-05-21, by wenzelm
Isamode and ProofGeneral configuration moved to Pure/Interface;
1999-05-21, by wenzelm
added use_thy_only;
1999-05-21, by wenzelm
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
1999-05-21, by wenzelm
avoid string constants;
1999-05-21, by wenzelm
qed indexed.
1999-05-21, by nipkow
typedef_proof: pass interactive flag;
1999-05-21, by wenzelm
tuned;
1999-05-21, by wenzelm
cleaned comments;
1999-05-21, by wenzelm
renamed 'begin' / 'end' to '{{' / '}}';
1999-05-21, by wenzelm
history commands;
1999-05-21, by wenzelm
tuned;
1999-05-21, by wenzelm
adapted to History changes;
1999-05-21, by wenzelm
local_qed: obtain interactive flag;
1999-05-21, by wenzelm
backup replaced by checkpoint;
1999-05-21, by wenzelm
added default_prompt;
1999-05-21, by wenzelm
optional limit;
1999-05-21, by wenzelm
improved errors;
1999-05-21, by wenzelm
updated comment
1999-05-21, by paulson
made definition more readable
1999-05-21, by paulson
preferring generic rules to specific ones...
1999-05-21, by paulson
changes to show that Lists are partially ordered by the prefix relation
1999-05-21, by paulson
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)
1999-05-21, by paulson
redid proofs to use "always" rather than "reachable" (somewhat)
1999-05-19, by paulson
new theorem Always_reachable
1999-05-19, by paulson
tuned;
1999-05-18, by wenzelm
added Locale paper
1999-05-18, by paulson
locale documentation (from Florian)
1999-05-18, by paulson
../manual.bib a new dependency
1999-05-18, by paulson
cleaned comments;
1999-05-17, by wenzelm
cleaned comments;
1999-05-17, by wenzelm
tuned;
1999-05-17, by wenzelm
cleaned comments;
1999-05-17, by wenzelm
ThyInfo.finalize_all renamed to ThyInfo.finish;
1999-05-17, by wenzelm
node_cases renamed to node_case;
1999-05-17, by wenzelm
prep_ext exported (again);
1999-05-17, by wenzelm
backup operation replaces transaction;
1999-05-17, by wenzelm
removed get_nodes;
1999-05-17, by wenzelm
remove_thy;
1999-05-17, by wenzelm
tuned arrows;
1999-05-17, by wenzelm
Arrows are no longer needed because of redesign of the
1999-05-17, by berghofe
Changed some file names.
1999-05-17, by berghofe
Added function get_preds.
1999-05-17, by berghofe
Added setup for BrowserInfo.
1999-05-17, by berghofe
usedir now recognizes additional option -P which is used to
1999-05-17, by berghofe
Changed interface of function use_dir.
1999-05-17, by berghofe
Present.begin_theory now needs an additional argument of type
1999-05-17, by berghofe
Reimplemented graph generator.
1999-05-17, by berghofe
Added some code to enable browser to display remote documents.
1999-05-17, by berghofe
new thm extend_JN; renamed extend_leadsto
1999-05-17, by paulson
"component" now an infix
1999-05-17, by paulson
indentation
1999-05-17, by paulson
tuned;
1999-05-15, by wenzelm
ad-hoc fix for bold indexes;
1999-05-12, by wenzelm
strip_quotes replaced by unenclose;
1999-05-12, by wenzelm
rearranged some modules;
1999-05-12, by wenzelm
rearranged order of modules;
1999-05-12, by wenzelm
Basic URLs.
1999-05-12, by wenzelm
added url.ML;
1999-05-12, by wenzelm
pdf setup;
1999-05-12, by wenzelm
tuned;
1999-05-12, by wenzelm
fixed msg;
1999-05-11, by wenzelm
moved scan.ML;
1999-05-11, by wenzelm
new comments, variable renaming, etc
1999-05-11, by paulson
tidied
1999-05-11, by paulson
changes for new manual.bib
1999-05-11, by paulson
make pdf;
1999-05-10, by wenzelm
tuned;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
cite HOLCF;
1999-05-10, by wenzelm
tuned;
1999-05-10, by wenzelm
axclass;
1999-05-10, by wenzelm
axclass;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
*** empty log message ***
1999-05-10, by wenzelm
*** empty log message ***
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
fixed URLs;
1999-05-10, by wenzelm
pdf setup;
1999-05-10, by wenzelm
replaced png by pdf;
1999-05-07, by wenzelm
pdf pics;
1999-05-07, by wenzelm
tidied
1999-05-07, by paulson
tidied
1999-05-07, by paulson
new refererences for Inductive manual, but still incomplete
1999-05-07, by paulson
tuned;
1999-05-06, by wenzelm
pdf setup;
1999-05-06, by wenzelm
*** empty log message ***
1999-05-06, by wenzelm
pdf setup;
1999-05-06, by wenzelm
tuned;
1999-05-06, by wenzelm
More refs.
1999-05-06, by nipkow
Refs.
1999-05-06, by nipkow
New title page.
1999-05-06, by nipkow
tuned;
1999-05-05, by wenzelm
manual.bib;
1999-05-05, by wenzelm
no rail;
1999-05-05, by wenzelm
fixed FILES;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
isabelle.eps;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
tuned;
1999-05-05, by wenzelm
improved Makefile;
1999-05-05, by wenzelm
*** empty log message ***
1999-05-05, by wenzelm
Common part for Doc Makefiles;
1999-05-05, by wenzelm
Now uses manual.bib; some references updated
1999-05-05, by paulson
tuned rpm file names;
1999-05-05, by wenzelm
updated docs;
1999-05-05, by wenzelm
Bibtex database for documentation.
1999-05-05, by nipkow
Bibtex stuff.
1999-05-05, by nipkow
*** empty log message ***
1999-05-04, by wenzelm
HOL;
1999-05-04, by wenzelm
removed HOL.tex;
1999-05-04, by wenzelm
tuned;
1999-05-04, by wenzelm
updated;
1999-05-04, by wenzelm
HOL part moved to 'logics-HOL' manual;
1999-05-04, by wenzelm
fixed;
1999-05-04, by wenzelm
used to be part of 'logics' manual;
1999-05-04, by wenzelm
isabelle_zf image;
1999-05-04, by wenzelm
*** empty log message ***
1999-05-04, by wenzelm
Arithmetic.
1999-05-04, by nipkow
add_recdef: removed names / attributes;
1999-05-04, by wenzelm
new definitions of Co and LeadsTo
1999-05-04, by paulson
transaction: Theory.copy;
1999-05-04, by wenzelm
hide prep_ext, merge_theories;
1999-05-04, by wenzelm
oops;
1999-05-04, by wenzelm
tuned;
1999-05-04, by wenzelm
Invariant -> Always and other tidying
1999-05-04, by paulson
tuned;
1999-05-03, by wenzelm
theory loader stuff updated and improved;
1999-05-03, by wenzelm
fixed reqs?
1999-05-03, by wenzelm
improved error handling
1999-05-03, by paulson
renamed state variables
1999-05-03, by paulson
tidied
1999-05-03, by paulson
tuned;
1999-05-03, by wenzelm
prefer /bin for ./configure;
1999-05-03, by wenzelm
try chown root:root;
1999-05-03, by wenzelm
renamed 'dummy' to 'dummy_pattern' (less dangerous);
1999-05-01, by wenzelm
tuned;
1999-04-30, by wenzelm
method = meth3 (again);
1999-04-30, by wenzelm
peoper defer_recdef interface;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
separated recdef / defer_recdef;
1999-04-30, by wenzelm
tuned defer_recdef interfaces;
1999-04-30, by wenzelm
comment, interest;
1999-04-30, by wenzelm
Comment.text;
1999-04-30, by wenzelm
comment sections;
1999-04-30, by wenzelm
dummy patterns;
1999-04-30, by wenzelm
added Isar/comment.ML;
1999-04-30, by wenzelm
val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
theory data: copy;
1999-04-30, by wenzelm
improved icons;
1999-04-30, by wenzelm
Isabelle icons;
1999-04-30, by wenzelm
patched sum_case;
1999-04-30, by wenzelm
Obsolete because JDK 1.1.x contains a class ScrollPane
1999-04-29, by berghofe
Updated to JDK 1.1.x
1999-04-29, by berghofe
Proof mods due to eta contraction during rewriting.
1999-04-29, by nipkow
Eta contraction is now performed all the time during rewriting.
1999-04-29, by nipkow
currently disabled;
1999-04-29, by wenzelm
*** empty log message ***
1999-04-29, by wenzelm
made many specification operators infix
1999-04-29, by paulson
eliminated theory UNITY/Traces
1999-04-28, by paulson
improper simp methods;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
fold / unfold methods;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
no Toplevel.print for by, ., ..;
1999-04-27, by wenzelm
improved print_state;
1999-04-27, by wenzelm
verbose flag;
1999-04-27, by wenzelm
use_thy_only made pervasive;
1999-04-27, by wenzelm
added Isar_examples/NatSum.thy;
1999-04-27, by wenzelm
Old stuff.
1999-04-27, by nipkow
proper quiet_mode;
1999-04-27, by wenzelm
adapted add_inductive, add_record;
1999-04-27, by wenzelm
adapted add_inductive;
1999-04-27, by wenzelm
intrs attributes;
1999-04-27, by wenzelm
proper quiet_mode;
1999-04-27, by wenzelm
iff_add_global (from simpdata.ML);
1999-04-27, by wenzelm
support forward chaining;
1999-04-27, by wenzelm
tuned;
1999-04-27, by wenzelm
added Isar_examples/Cantor.ML;
1999-04-27, by wenzelm
hol_setup, simpdata_setup;
1999-04-27, by wenzelm
"iff" attribute;
1999-04-27, by wenzelm
hol_setup;
1999-04-27, by wenzelm
"!" made keyword;
1999-04-27, by wenzelm
opt_thm_name: name optional;
1999-04-27, by wenzelm
added oooo;
1999-04-27, by wenzelm
fixed a bug many years old in rule plusEC
1999-04-26, by paulson
tuned msgs;
1999-04-26, by wenzelm
tuned;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
elaborated;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
tuned antiquotations;
1999-04-23, by wenzelm
improved 'single' method;
1999-04-23, by wenzelm
added thus, hence;
1999-04-23, by wenzelm
added FINISHED, same_tac;
1999-04-23, by wenzelm
use /usr/share and /usr/bin;
1999-04-23, by wenzelm
Now for recdefs that omit the WF relation;
1999-04-23, by paulson
Now for recdefs that omit the WF relation
1999-04-23, by paulson
Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml
1999-04-23, by paulson
chgrp isabelle;
1999-04-23, by wenzelm
detailed proofs;
1999-04-23, by wenzelm
tuned;
1999-04-23, by wenzelm
oops;
1999-04-23, by wenzelm
fixed IO;
1999-04-22, by wenzelm
improved load paths;
1999-04-22, by wenzelm
single method: include not_elim, imp_elim;
1999-04-22, by wenzelm
more graceful handling of load paths;
1999-04-22, by wenzelm
improved auto dir handling;
1999-04-22, by wenzelm
tuned;
1999-04-22, by wenzelm
make Isabelle rpm packages for Linux/x86 from the distribution;
1999-04-22, by wenzelm
use_thy etc.: may specify path prefix, which is temporarily used as load path;
1999-04-22, by wenzelm
switch_theory: Context.pass;
1999-04-22, by wenzelm
recdef (TFL) now requires theory Recdef;
1999-04-22, by wenzelm
recdef requires theory Recdef;
1999-04-22, by wenzelm
tuned;
1999-04-22, by wenzelm
rep_datatype syntax: 'induction' instead of 'induct';
1999-04-22, by wenzelm
add_recdef: actual simpset;
1999-04-22, by wenzelm
recdef adapted to RecdefPackage.add_recdef;
1999-04-22, by wenzelm
Theory.requires changed to "Recdef" and moved to HOL/Tools/recdef_package.ML;
1999-04-22, by wenzelm
added ex and Modelcheck
1999-04-22, by mueller
tuned;
1999-04-22, by wenzelm
added for mucke translation;
1999-04-22, by mueller
deleted some old examples in Modelcheck;
1999-04-22, by mueller
added translation from IOA to mucalculus and corresponding modelchecker examples;
1999-04-22, by mueller
moved this trivial example to new ex dir;
1999-04-22, by mueller
changed to include new subdirs ex and Modelcheck;
1999-04-22, by mueller
put types into "" because of signature clash;
1999-04-22, by mueller
added frontend syntax for IOA, moved trivial examples to folder ex;
1999-04-22, by mueller
added modelchecker mucke besides modelchecker eindhoven;
1999-04-22, by mueller
delete old files for adding second modelchecker connection;
1999-04-22, by mueller
$ML_HOME/.arch-n-opsys 2>/dev/null;
1999-04-21, by wenzelm
smlnj-110 setup made default;
1999-04-21, by wenzelm
/usr/share/smlnj/bin;
1999-04-21, by wenzelm
Isamode 2.6 requires patch;
1999-04-21, by wenzelm
added is_current;
1999-04-21, by wenzelm
fixed ISABELLE_HOME/lib/logo/isabelle-tiny.xpm;
1999-04-20, by wenzelm
temporarily fake quiet_mode;
1999-04-20, by wenzelm
temporarily reverted to 1.24;
1999-04-20, by wenzelm
IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly)
1999-04-20, by paulson
Main is the correct parent
1999-04-20, by paulson
new result extend_LeadsTo
1999-04-20, by paulson
should not refer to Datatype
1999-04-20, by paulson
addition of Kerberos IV example
1999-04-20, by paulson
tidied
1999-04-20, by paulson
improved usage;
1999-04-19, by wenzelm
loadpath replaced;
1999-04-16, by wenzelm
and_list;
1999-04-16, by wenzelm
lifted enum;
1999-04-16, by wenzelm
may specify induction predicates as well;
1999-04-16, by wenzelm
added Isar_examples;
1999-04-16, by wenzelm
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
1999-04-16, by wenzelm
lemmas about proper subset relation;
1999-04-16, by wenzelm
Proof by induction on types / set / functions.
1999-04-16, by wenzelm
print_datatypes;
1999-04-16, by wenzelm
added Tools/induct_method.ML;
1999-04-16, by wenzelm
'HOL/recdef' theory data;
1999-04-16, by wenzelm
'HOL/recdef' theory data;
1999-04-16, by wenzelm
'HOL/inductive' theory data;
1999-04-16, by wenzelm
Sign.base_name fid;
1999-04-16, by wenzelm
added incr_indexes, incr_indexes_wrt;
1999-04-16, by wenzelm
Proof mod.
1999-04-15, by nipkow
Added new thms.
1999-04-15, by nipkow
quiet_mode;
1999-04-14, by wenzelm
Tools/inductive_package.ML;
1999-04-14, by wenzelm
triple_swap;
1999-04-14, by wenzelm
Wrapper module for Konrad Slind's TFL package.
1999-04-14, by wenzelm
remoced old set_current_thy;
1999-04-14, by wenzelm
tuned messages;
1999-04-14, by wenzelm
intrs: names and atts;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
tuned comments;
1999-04-14, by wenzelm
intrs: provide names and atts;
1999-04-14, by wenzelm
cleaned comments;
1999-04-14, by wenzelm
tuned;
1999-04-14, by wenzelm
fixed named type infixes (actual BUG!);
1999-04-14, by wenzelm
updated isatool install;
1999-04-13, by wenzelm
-p option;
1999-04-13, by wenzelm
adapted isatool install;
1999-04-13, by wenzelm
improved isatool install;
1999-04-13, by wenzelm
tuned;
1999-04-13, by wenzelm
ML_PLATFORM;
1999-04-12, by wenzelm
ML_PLATFORM;
1999-04-12, by wenzelm
fixed @@;
1999-04-07, by wenzelm
fixed bib file
1999-04-04, by paulson
fixed;
1999-04-03, by wenzelm
new definition for nth.
1999-04-01, by pusch
useless relic
1999-03-31, by nipkow
arith_tac
1999-03-30, by nipkow
tuned;
1999-03-19, by wenzelm
common qed and end of proofs;
1999-03-19, by wenzelm
* New bounded quantifier syntax (input only):
1999-03-18, by nipkow
New bounded quantifier syntax: !x<i. P etc
1999-03-18, by nipkow
added new theory Yahalom_Bad
1999-03-18, by paulson
added new theory Yahalom_Bad
1999-03-18, by paulson
exchanged the order of Gets and Notes in datatype event
1999-03-18, by paulson
fixed thm_name again;
1999-03-17, by wenzelm
Theory.sign_of;
1999-03-17, by wenzelm
xnum token class;
1999-03-17, by wenzelm
xstr token class;
1999-03-17, by wenzelm
Theory.sign_of;
1999-03-17, by wenzelm
fixed axclass_tac;
1999-03-17, by wenzelm
tuned;
1999-03-17, by wenzelm
Theory.sign_of;
1999-03-17, by wenzelm
qualify Theory.sign_of etc.;
1999-03-17, by wenzelm
fixed msg;
1999-03-17, by wenzelm
tuned msg;
1999-03-17, by wenzelm
axclass_tac lost an argument;
1999-03-17, by wenzelm
HOL/typedef: fixed type inference for representing set;
1999-03-17, by wenzelm
rep_datatype: '_i' version, attributes, outer syntax;
1999-03-17, by wenzelm
local open OuterParse;
1999-03-17, by wenzelm
actually check non-emptiness theorem;
1999-03-17, by wenzelm
fixed typedef representing set;
1999-03-17, by wenzelm
adapted rep_datatype;
1999-03-17, by wenzelm
added dest_mem;
1999-03-17, by wenzelm
theory data;
1999-03-17, by wenzelm
adapted AxClass.add_axclass;
1999-03-17, by wenzelm
tuned msgs;
1999-03-17, by wenzelm
tuned;
1999-03-17, by wenzelm
cleaned comments;
1999-03-17, by wenzelm
added apply_cond_open;
1999-03-17, by wenzelm
added (improper_)command;
1999-03-17, by wenzelm
added simple_arity, spec_name, spec_opt_name;
1999-03-17, by wenzelm
added '_i' versions;
1999-03-17, by wenzelm
OuterSyntax.(improper_)command;
1999-03-17, by wenzelm
added assert_super;
1999-03-17, by wenzelm
added def_name;
1999-03-17, by wenzelm
added cond_extern_thm_sg;
1999-03-17, by wenzelm
AxClass.setup;
1999-03-17, by wenzelm
axclass.ML loaded after Isar;
1999-03-17, by wenzelm
made weblint happy;
1999-03-12, by wenzelm
comment;
1999-03-12, by wenzelm
removed obsolete user data stuff;
1999-03-12, by wenzelm
theory: include parent links;
1999-03-12, by wenzelm
outer syntax for 'datatype';
1999-03-11, by wenzelm
add_primrec(_i): attributes;
1999-03-11, by wenzelm
outer syntax for 'record';
1999-03-11, by wenzelm
named witnesses: PureThy.get_thmss;
1999-03-11, by wenzelm
primrec: empty attributes;
1999-03-11, by wenzelm
tuned opt_mixfix failure;
1999-03-11, by wenzelm
add_title;
1999-03-11, by wenzelm
added 'title';
1999-03-11, by wenzelm
tuned space;
1999-03-11, by wenzelm
comment;
1999-03-11, by wenzelm
workaround default_name problem;
1999-03-11, by wenzelm
removed foo_build_completed -- now handled by session management (via usedir);
1999-03-11, by wenzelm
include 'README';
1999-03-11, by wenzelm
tuned;
1999-03-11, by wenzelm
moved Thy/session.ML to Isar/session.ML;
1999-03-11, by wenzelm
tuned;
1999-03-10, by wenzelm
-x option;
1999-03-10, by wenzelm
updated;
1999-03-10, by wenzelm
report session path;
1999-03-10, by wenzelm
report path instead of actual session;
1999-03-10, by wenzelm
HTML output;
1999-03-10, by wenzelm
maintain current/parent index;
1999-03-10, by wenzelm
output: some symbol translations;
1999-03-10, by wenzelm
parent_session;
1999-03-10, by wenzelm
allow meta_outer to do nothing
1999-03-10, by paulson
updating both Yahalom protocols to the Gets model
1999-03-10, by paulson
updated not_bad_tac for the Gets model
1999-03-10, by paulson
deleted obsolete comments
1999-03-10, by paulson
Present.theory_source;
1999-03-09, by wenzelm
begin/end_theory: presentation;
1999-03-09, by wenzelm
checkpoint -- basic functionality only;
1999-03-09, by wenzelm
added use_path;
1999-03-09, by wenzelm
IsarThy.begin/end_theory;
1999-03-09, by wenzelm
Present.theorem;
1999-03-09, by wenzelm
fixed add_path reset;
1999-03-09, by wenzelm
still fake, passes BrowserInfo;
1999-03-09, by wenzelm
HTML markup elements.
1999-03-09, by wenzelm
added html.ML, browser_info.ML;
1999-03-09, by wenzelm
token translation: real;
1999-03-09, by wenzelm
added strlen_real, setmp_margin;
1999-03-09, by wenzelm
tuned using nth_elem_string, exists_string;
1999-03-09, by wenzelm
added make, dir;
1999-03-09, by wenzelm
added mkdir;
1999-03-09, by wenzelm
added Buffer;
1999-03-09, by wenzelm
simple string buffers;
1999-03-09, by wenzelm
*** empty log message ***
1999-03-09, by wenzelm
pretty_thm_no_quote;
1999-03-09, by wenzelm
HTML.setup;
1999-03-09, by wenzelm
added nth_elem_string, exists_string;
1999-03-09, by wenzelm
token translation: real;
1999-03-09, by wenzelm
tuned;
1999-03-09, by wenzelm
tidied
1999-03-09, by paulson
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
1999-03-09, by paulson
Suc -> +1
1999-03-08, by nipkow
modified zip
1999-03-08, by nipkow
Fixed bug in add_datatype_axm:
1999-03-05, by berghofe
fixed again;
1999-03-04, by wenzelm
expandshort
1999-03-03, by paulson
added UNITY/Extend
1999-03-03, by paulson
expandshort
1999-03-03, by paulson
tidied
1999-03-03, by paulson
UNITY fully working at last...
1999-03-03, by paulson
expandshort
1999-03-03, by paulson
new theory of extending the state space
1999-03-03, by paulson
fixed {ISABELLE};
1999-03-01, by wenzelm
removed the infernal States, eqStates, compatible, etc.
1999-03-01, by paulson
tidied
1999-03-01, by paulson
simpler proofs of congruence rules
1999-03-01, by paulson
new results e.g. about Pow; new simprules Union_image_eq, Inter_image_eq
1999-03-01, by paulson
simpler proofs of congruence rules
1999-03-01, by paulson
new image laws
1999-02-22, by paulson
added a commment on the "ext" rule
1999-02-22, by paulson
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
1999-02-22, by paulson
added rev_bexI
1999-02-22, by paulson
fixed order of multiple -m options;
1999-02-18, by wenzelm
fixed geometry;
1999-02-18, by grobauer
tidying in conjuntion with the TISSEC paper; replaced (unit option)
1999-02-16, by paulson
new theorem image_Union_eq
1999-02-16, by paulson
foldl_string;
1999-02-13, by wenzelm
renamed space2 to spacespace
1999-02-12, by oheimb
tuned pretty format lookup;
1999-02-12, by wenzelm
pretty_thm: quote terms (separately);
1999-02-12, by wenzelm
Symbol.output subject to print mode;
1999-02-11, by wenzelm
-m isabelle_font;
1999-02-11, by wenzelm
tuned;
1999-02-11, by wenzelm
Present.init;
1999-02-11, by wenzelm
init, finish;
1999-02-11, by wenzelm
proper handling of print_mode wrt. Pretty.sym;
1999-02-11, by wenzelm
added output_width;
1999-02-11, by wenzelm
sym: Symbol.output_width;
1999-02-11, by wenzelm
val appends: T list -> T;
1999-02-11, by wenzelm
tuned;
1999-02-11, by wenzelm
tidied; better error messages
1999-02-09, by paulson
new lemma surjD
1999-02-09, by paulson
Context.fetch, Context.setmp;
1999-02-08, by wenzelm
"files" keyword!
1999-02-08, by wenzelm
use: provide context;
1999-02-08, by wenzelm
tuned msgs;
1999-02-08, by wenzelm
tuned msg;
1999-02-08, by wenzelm
added fetch, fetch_theory;
1999-02-08, by wenzelm
~~;
1999-02-08, by wenzelm
path element specification '~~' refers to '$ISABELLE_HOME';
1999-02-08, by wenzelm
no deps on compile time sources;
1999-02-08, by wenzelm
isatool logo;
1999-02-08, by wenzelm
-i option;
1999-02-08, by wenzelm
updated (Stephan Merz);
1999-02-08, by wenzelm
updated TLA;
1999-02-08, by wenzelm
made MLWorks happy;
1999-02-05, by wenzelm
examples made separate dirs;
1999-02-05, by wenzelm
add_path;
1999-02-05, by wenzelm
Hyperreal made part of Real;
1999-02-05, by wenzelm
Session.use_dir: check parent;
1999-02-05, by wenzelm
*** empty log message ***
1999-02-05, by wenzelm
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip