isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -120 +120 +1000 +3000 +10000 +30000 tip

extend_theory: changed type of "abbrs" arg;
1994-02-03, by wenzelm
made error message "file not found" more informative
1994-02-02, by clasohm
case was renamed to sum_case
1994-01-26, by nipkow
added is_empty: env -> bool, minidx: env -> int option;
1994-01-24, by wenzelm
added HOLCF
1994-01-20, by nipkow
removed square and fact
1994-01-20, by nipkow
HOLCF examples
1994-01-19, by nipkow
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
1994-01-19, by nipkow
commented out sig constraint of functor (for debugging purposes);
1994-01-19, by wenzelm
changed SYNTAX_FILES;
1994-01-19, by wenzelm
contains remaining parts of xgram.ML and extension.ML;
1994-01-19, by wenzelm
minor internal changes;
1994-01-19, by wenzelm
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
1994-01-19, by wenzelm
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
1994-01-19, by wenzelm
added some utils: commas, breaks, fbreaks, block, parents, list, str_list;
1994-01-19, by wenzelm
cosmetic changes;
1994-01-19, by wenzelm
minor cleanup;
1994-01-19, by wenzelm
major cleanup and reorganisation;
1994-01-19, by wenzelm
corrected comment
1994-01-18, by lcp
Updated refs to old Sign functions
1994-01-18, by lcp
Many other files modified as follows:
1994-01-18, by lcp
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
1994-01-18, by lcp
some optimizations of Larry's
1994-01-18, by nipkow
corrected comments
1994-01-14, by lcp
corrected comments
1994-01-14, by lcp
optimized net for matching of abstractions to speed up simplifier
1994-01-14, by nipkow
moved misplaced comment
1994-01-11, by nipkow
removed Syntax/parse_tree.ML;
1994-01-11, by wenzelm
optimized the number of eta-contractions in rewriting
1994-01-11, by nipkow
added a check for existence of a temporary file before removing it
1994-01-10, by clasohm
used unlink for delete_files instead of calling rm
1994-01-10, by clasohm
commented out sig constraint of functor (for debugging purposes);
1994-01-10, by wenzelm
ZF/perm/image_comp: new
1994-01-07, by lcp
got rid of METAHYPS due to the change of the basic simplification routines
1994-01-05, by nipkow
adapted a proof to the new solver (see change of FOL/simpdata.ML)
1994-01-05, by nipkow
updated solver of FOL_ss. see change of HOL/simpdata.ML
1994-01-05, by nipkow
added new parameter to the simplification tactics which indicates if
1994-01-05, by nipkow
added lexical class of type variables
1994-01-05, by nipkow
shortened msg
1994-01-05, by nipkow
added fake_cterm_of to speed up rewriting
1994-01-04, by nipkow
commented out sig constraint of functor (for debugging purposes);
1994-01-04, by wenzelm
changed tracing of simplifier
1994-01-04, by nipkow
optimized simplifier - signature of rewritten term stays constant
1994-01-02, by nipkow
added "Reading thy-File" message
1993-12-30, by clasohm
added subsig: sg * sg -> bool to test if one signature is contained in another.
1993-12-30, by nipkow
added sys_error;
1993-12-29, by wenzelm
fixed a bug in update/next_level which occured when a child wasn't loaded
1993-12-22, by clasohm
added empty type-abbr field to extend_theory
1993-12-21, by nipkow
added []-field to extend_theory: no type abbreviations.
1993-12-21, by nipkow
Added []-field to extend_theory to accomodate type abbreviations.
1993-12-21, by nipkow
Necessary changes to accomodate type abbreviations.
1993-12-21, by nipkow
pretty_thm is now exported;
1993-12-21, by wenzelm
new section for equality properties
1993-12-21, by lcp
Updated read_insts to approximate simultaneous type checking of substitution
1993-12-14, by nipkow
added isabelle-users paragraph
1993-12-13, by lcp
added mention of simplifier, splitter, hypsubst
1993-12-13, by lcp
new year
1993-12-13, by lcp
updated instantiate to deal with type clashes
1993-12-10, by nipkow
ZF/equalities/SUM_eq_UN: new
1993-12-10, by lcp
Pure/tactic/compose_inst_tac: when catching exception THM, prints the
1993-12-10, by lcp
deleted harmful basify, which pulled rewrite rules down to base type.
1993-12-09, by nipkow
added rep_tsig Isabelle93
1993-12-06, by nipkow
last minute changes, eg literal tokens -> delimiters and valued tokens ->
1993-12-06, by nipkow
ZF/univ/in_Vfrom_limit: new
1993-12-06, by lcp
ZF/ord/Ord_Un,Ord_Int,Un_upper1_le,Un_upper2_le: new
1993-12-06, by lcp
Typos and style
1993-12-06, by nipkow
Changed Acknowledgements
1993-12-03, by lcp
Acknowledged Carsten Clasohm
1993-12-03, by lcp
New distributive laws for Sigma and UN
1993-12-03, by lcp
removal of amssymbols.sty and lcp.sty; addition of iman.sty
1993-12-02, by lcp
ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
1993-12-01, by lcp
minor corrections
1993-12-01, by lcp
new references
1993-12-01, by lcp
now inspects FOLP_build_completed
1993-12-01, by lcp
now declares FOLP_build_completed
1993-12-01, by lcp
*** empty log message ***
1993-11-30, by wenzelm
*** empty log message ***
1993-11-30, by wenzelm
ZF/ex/llist_eq/lleq_Int_Vset_subset_lemma,
1993-11-30, by lcp
changed split_filename, remove_ext;
1993-11-30, by wenzelm
*** empty log message ***
1993-11-30, by wenzelm
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
1993-11-30, by lcp
extend: cleaned up, adapted for new Syntax.extend;
1993-11-29, by wenzelm
*** empty log message ***
1993-11-29, by wenzelm
added (partial) extend_tables;
1993-11-29, by wenzelm
changed datatype ext;
1993-11-29, by wenzelm
improved comments;
1993-11-29, by wenzelm
added SCANNER;
1993-11-29, by wenzelm
added Scanner;
1993-11-29, by wenzelm
added logical_types
1993-11-29, by nipkow
improved comments;
1993-11-29, by wenzelm
added equal, not_equal: ''a -> ''a -> bool
1993-11-29, by wenzelm
Minor edits to discussion of use_thy
1993-11-26, by lcp
Correction to eta-contraction; thanks to Markus W.
1993-11-26, by lcp
Correction to page 16; thanks to Markus W.
1993-11-26, by lcp
Corrected errors found by Marcus Wenzel.
1993-11-26, by lcp
changed some names and deleted *NORMALIZED*
1993-11-25, by nipkow
corrected obvious errors;
1993-11-25, by wenzelm
corrected obvious errors;
1993-11-25, by wenzelm
*** empty log message ***
1993-11-25, by wenzelm
corrected some obvious errors;
1993-11-25, by wenzelm
changed beginning of "Reading a new theory", added index "automatic loading"
1993-11-25, by clasohm
corrected trivial typo;
1993-11-25, by wenzelm
corrected trivial typo;
1993-11-25, by wenzelm
fixed a bug in get_filenames, changed output of use_thy
1993-11-25, by clasohm
asm_full_simp_tac now fails if there are no subgoals
1993-11-25, by nipkow
added subsection 'Classes and types';
1993-11-25, by wenzelm
added Syntax.read_typ;
1993-11-25, by wenzelm
Sign.extend: Syntax.extend now called with read_ty;
1993-11-25, by wenzelm
removed section 'Classes and types';
1993-11-25, by wenzelm
added index commands, removed last paragraph of "Using Poly/ML"
1993-11-25, by clasohm
changed itmath trickery to be compatible with NFSS (itmath.sty)
1993-11-23, by nipkow
minor changes
1993-11-22, by nipkow
added chapter "Defining Theories" and made changes for new Readthy functions
1993-11-22, by clasohm
*** empty log message ***
1993-11-22, by wenzelm
*** empty log message ***
1993-11-22, by wenzelm
various minor changes;
1993-11-22, by wenzelm
Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
1993-11-22, by nipkow
Reformatting of SIMPLIFIER figure
1993-11-19, by lcp
Trivial spacing corrections
1993-11-19, by lcp
Documents not, and, or, xor: boolean ops
1993-11-19, by lcp