isabelle: Graph

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
more robust handling of theory context;
1999-02-05, by wenzelm
improved theory, context, update_context;
1999-02-05, by wenzelm
improved 'theory';
1999-02-05, by wenzelm
improved msg;
1999-02-05, by wenzelm
use_thy, update_thy: Context.save;
1999-02-05, by wenzelm
tuned;
1999-02-05, by wenzelm
time_use made pervasive;
1999-02-05, by wenzelm
use_dir: check parent, more robust exit;
1999-02-05, by wenzelm
more robust RC;
1999-02-05, by wenzelm
setmp: theory option;
1999-02-05, by wenzelm
Session.finish ();
1999-02-05, by wenzelm
tidied Schroeder-Bernstein proof
1999-02-05, by paulson
new surj rules
1999-02-05, by paulson
obsolete;
1999-02-04, by wenzelm
tuned;
1999-02-04, by wenzelm
include full paths in file info;
1999-02-04, by wenzelm
Symbol.use;
1999-02-04, by wenzelm
Symbol.use (eliminated Use.exit_use);
1999-02-04, by wenzelm
leave theory context after load_thy;
1999-02-04, by wenzelm
File.pwd, File.cd;
1999-02-04, by wenzelm
fixed file_info;
1999-02-04, by wenzelm
use, cd;
1999-02-04, by wenzelm
added 'use';
1999-02-04, by wenzelm
fail_safe close;
1999-02-04, by wenzelm
check_elem: allow ~, except for '~' and '~~';
1999-02-04, by wenzelm
removed use.ML;
1999-02-04, by wenzelm
removed General/use.ML;
1999-02-04, by wenzelm
made SML/NJ happy;
1999-02-03, by wenzelm
check_thy: include ML stamp;
1999-02-03, by wenzelm
added join_info;
1999-02-03, by wenzelm
tidied load path handling;
1999-02-03, by wenzelm
add_path / reset_path;
1999-02-03, by wenzelm
tuned;
1999-02-03, by wenzelm
ThmDatabase.ml_store_thm;
1999-02-03, by wenzelm
usedir -r;
1999-02-03, by wenzelm
Session.init;
1999-02-03, by wenzelm
Theory loader database: theory and file dependencies, theory values
1999-02-03, by wenzelm
tidied;
1999-02-03, by wenzelm
Session management -- maintain state of logic images.
1999-02-03, by wenzelm
get_lexicon;
1999-02-03, by wenzelm
tokenize: get exploded args;
1999-02-03, by wenzelm
delete_tmpfiles (from thy_read.ML);
1999-02-03, by wenzelm
added reset_path;
1999-02-03, by wenzelm
open BasicThmDatabase;
1999-02-03, by wenzelm
Theory presentation (fake implementation);
1999-02-03, by wenzelm
moved to Pure/context.ML;
1999-02-03, by wenzelm
nuked;
1999-02-03, by wenzelm
moved to General/use.ML;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
ThyInfo.begin_theory;
1999-02-03, by wenzelm
oops, update_thy;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
comment;
1999-02-03, by wenzelm
removed load;
1999-02-03, by wenzelm
proper setup of preloaded theories (ThyInfo.register_theory);
1999-02-03, by wenzelm
renamed sig to PRIVATE_SIGN;
1999-02-03, by wenzelm
added thm, thms, Open_locale, Close_locale, Print_scope;
1999-02-03, by wenzelm
added Goal(w) and Export (from context.ML);
1999-02-03, by wenzelm
added is_draft;
1999-02-03, by wenzelm
enabled sig;
1999-02-03, by wenzelm
tuned msg;
1999-02-03, by wenzelm
Global theory context (used to be in Thy/context.ML);
1999-02-03, by wenzelm
moved several files;
1999-02-03, by wenzelm
more abstract implementation;
1999-02-03, by wenzelm
use Path.T;
1999-02-03, by wenzelm
of_file: Path.T, Position.T;
1999-02-03, by wenzelm
added use.ML;
1999-02-03, by wenzelm
added Use;
1999-02-03, by wenzelm
tuned;
1999-02-03, by wenzelm
tidied; added thy_load.ML
1999-02-03, by paulson
tidied, with left_inverse & right_inverse as default simprules
1999-02-03, by paulson
auto update
1999-02-03, by paulson
inj
1999-02-03, by paulson
documented typecheck_tac, etc
1999-02-03, by paulson
standard spelling: type-checking
1999-02-03, by paulson
inj is now a translation of inj_on
1999-02-03, by paulson
standard spelling: type-checking
1999-02-03, by paulson
a bit of tidying
1999-02-01, by paulson
Theory loader primitives.
1999-01-30, by wenzelm
corrected output of symbols for several (probably not all) relevant functions
1999-01-29, by oheimb
renamed space2 to spacespace
1999-01-29, by oheimb
corrected output of symbols for several (probably not all) relevant functions
1999-01-29, by oheimb
moved print_mode to ROOT.ML
1999-01-29, by oheimb
expandshort
1999-01-29, by paulson
expandshort
1999-01-29, by paulson
tidied
1999-01-29, by paulson
tidied
1999-01-28, by paulson
constdefs
1999-01-28, by paulson
tidying
1999-01-28, by paulson
arith_tac for min/max
1999-01-27, by nipkow
*** empty log message ***
1999-01-27, by wenzelm
ZF typechecking
1999-01-27, by paulson
automatic insertion of datatype intr rules into claset
1999-01-27, by paulson
new typechecking solver for the simplifier
1999-01-27, by paulson
tuned;
1999-01-25, by wenzelm
Fixed a bug in lin.arith.
1999-01-24, by nipkow
tuned;
1999-01-22, by wenzelm