Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
+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.
syntax_error now checks precedences when computing expected tokens
1994-05-13, by clasohm
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
1994-05-13, by lcp
make-all-poly, make-all-nj: restored to main directory as examples
1994-05-13, by lcp
changed implode to ^
1994-05-11, by clasohm
moved 'filter is_xid' in syn_ext
1994-05-11, by clasohm
syntax_error now removes duplicate tokens in its output and doesn't
1994-05-09, by clasohm
ZF/indrule/mk_pred_typ: corrected pattern to include Abs, allowing it to
1994-05-06, by lcp
renaming/removal of filenames to correct case
1994-05-06, by lcp
renaming/removal of filenames to correct case
1994-05-06, by lcp
renaming/removal of filenames to correct case
1994-05-06, by lcp
improved syntax error:
1994-05-06, by clasohm
CTT.ML/SumE_fst,SumE_snd: tidied
1994-05-04, by lcp
Bool.ML: replaced many rewrite_goals_tac calls by prove_goalw
1994-05-04, by lcp
final Springer version
1994-05-03, by lcp
post-CRC corrections
1994-05-03, by lcp
post-CRC corrections
1994-05-03, by lcp
post-CRC corrections
1994-05-03, by lcp
post-CRC corrections
1994-05-03, by lcp
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
1994-05-03, by lcp
removal of obsolete type-declaration syntax
1994-05-03, by lcp
removal of obsolete type-declaration syntax
1994-05-03, by lcp
removal of obsolete type-declaration syntax
1994-05-03, by lcp
post-CRC corrections
1994-05-03, by lcp
post-CRC corrections
1994-05-03, by lcp
post-CRC corrections
1994-05-03, by lcp
changed translation of type applications according to new grammar;
1994-05-02, by wenzelm
added many more filenames to FILES and EX_FILES
1994-04-27, by lcp
made a few cosmetic changes
1994-04-26, by clasohm
final Springer copy
1994-04-25, by lcp
final Springer copy
1994-04-25, by lcp
renamed theory files
1994-04-24, by clasohm
fixed a small bug
1994-04-24, by clasohm
changed convention for theory file names: they now have to consist of the
1994-04-24, by clasohm
renamed theory files
1994-04-22, by clasohm
renamed theory files
1994-04-22, by clasohm
renamed theory files
1994-04-22, by clasohm
renamed theory files
1994-04-22, by clasohm
renamed theory files
1994-04-22, by clasohm
renamed theory files
1994-04-22, by clasohm
final Springer copy
1994-04-22, by lcp
final Springer copy
1994-04-22, by lcp
final Springer copy
1994-04-22, by lcp
changed the way a grammar is generated to allow the new parser to work;
1994-04-22, by clasohm
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
penultimate Springer draft
1994-04-15, by lcp
restored the signature constraint :THM
1994-04-06, by lcp
modifications towards final draft
1994-04-04, by lcp
modifications towards final draft
1994-04-04, by lcp
changed lists and added "let" and "case"
1994-03-30, by nipkow
Changed term ordering for permutative rewrites to be AC-compatible.
1994-03-27, by nipkow
revisions to first Springer draft
1994-03-24, by lcp
added section on type synonyms
1994-03-24, by nipkow
minor problems
1994-03-24, by nipkow
added \iflabelundefined
1994-03-24, by lcp
removed inconsistency with new HOL version
1994-03-24, by nipkow
Franz fragen
1994-03-24, by nipkow
structural induction for strict lists
1994-03-24, by nipkow
Franz fragen
1994-03-24, by nipkow
revisions to first Springer draft
1994-03-24, by lcp
have broken line
1994-03-23, by nipkow
final CADE version
1994-03-23, by lcp
first draft of Springer volume
1994-03-23, by lcp
first draft of Springer volume
1994-03-23, by lcp
first draft of Springer volume
1994-03-23, by lcp
changed "." to "$" and added parentheses to eliminate ambiguity
1994-03-22, by clasohm
changed "." to "$" to eliminate ambiguity
1994-03-22, by clasohm
Implemented "ordered rewriting": rules which merely permute variables, such
1994-03-22, by nipkow
first draft of Springer book
1994-03-21, by lcp
first draft of Springer book
1994-03-21, by lcp
first draft of Springer book
1994-03-21, by lcp
First draft of Springer book
1994-03-19, by lcp
new type declaration syntax instead of numbers
1994-03-17, by lcp
FOL/simpdata: tidied
1994-03-17, by lcp
CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD
1994-03-17, by lcp
CCL/ccl.ML/po_refl_iff_T: deleted reference to make_iff_T
1994-03-17, by lcp
Improved layout for inductive defs
1994-03-17, by lcp
adapted type definition to new syntax
1994-03-17, by clasohm
fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
1994-03-04, by wenzelm
changed "x" to "uu" for implicit name of the
1994-03-03, by lcp
update towards LNCS
1994-03-01, by nipkow
deleted a comment
1994-03-01, by nipkow
*** empty log message ***
1994-02-26, by nipkow
improved explode_tr;
1994-02-21, by wenzelm
minor update because HOL-lemma changed
1994-02-16, by nipkow
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
1994-02-16, by lcp
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
1994-02-16, by clasohm
double_complement_Un: new
1994-02-14, by lcp
*** empty log message ***
1994-02-09, by wenzelm
improved eq_sg;
1994-02-08, by wenzelm
added eq_set;
1994-02-08, by wenzelm
correction to cut tactics
1994-02-04, by lcp
no longer removes *.z
1994-02-03, by lcp
now makes HOLCF
1994-02-03, by lcp
added strs, big_list, writeln;
1994-02-03, by wenzelm
added simple_string_of_typ, simple_pprint_typ;
1994-02-03, by wenzelm
added type 'syntax';
1994-02-03, by wenzelm
minor internal changes;
1994-02-03, by wenzelm
syntax for type abbreviations;
1994-02-03, by wenzelm
(this is a preliminary release)
1994-02-03, by wenzelm
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
1994-02-03, by wenzelm
replaced pprint_sg by Sign.pprint_sg;
1994-02-03, by wenzelm
replaced eq_sg by Sign.eq_sg;
1994-02-03, by wenzelm
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
1994-02-03, by wenzelm
major cleanup;
1994-02-03, by wenzelm
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
Many edits suggested by Grundy & Thompson
1993-11-19, by lcp
expandshort and other trivial changes
1993-11-19, by lcp
expandshort
1993-11-18, by lcp
Misc modifs such as expandshort
1993-11-18, by lcp
added loaded_thys to signature and removed list_/set_loaded
1993-11-16, by clasohm
changed use_thy's parameter to exact theory name
1993-11-16, by clasohm
made pseudo theories for all ML files;
1993-11-16, by clasohm
moved call of store_theory to end of use t.thy; use t.ML;
1993-11-16, by clasohm
replaced \un by \union in "Simplification sets"
1993-11-16, by clasohm
changed use_thy's parameter to exact theory name
1993-11-16, by clasohm
changed all co- and co_ to co
1993-11-15, by lcp
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
1993-11-15, by lcp
Added commentary
1993-11-15, by lcp
fun parents: removed pp block (didn't have any effect)
1993-11-15, by wenzelm
changed application format for pretty-printer
1993-11-14, by nipkow
Misc updates
1993-11-12, by lcp
Misc updates
1993-11-12, by lcp
changed formatting for application
1993-11-11, by nipkow
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
1993-11-11, by nipkow
Various updates for Isabelle-93
1993-11-11, by lcp
new style file
1993-11-11, by lcp
adapted "Defining theories" to new use_thy
1993-11-11, by clasohm
replaced by current version;
1993-11-11, by wenzelm
replaced by current version;
1993-11-11, by wenzelm
*** empty log message ***
1993-11-11, by wenzelm
Initial revision
1993-11-10, by lcp
Initial revision
1993-11-10, by lcp
Initial revision
1993-11-09, by lcp
Target "test" now depends on examples files
1993-11-09, by lcp
Target "test" now depends on examples files
1993-11-09, by lcp
fixed a bug in POLY.ML: delete_file didn't close streams;
1993-11-09, by clasohm
renamed hard-quant.ML to hardquant.ML
1993-11-09, by clasohm
renamed int-prover.ML to intprover.ML,
1993-11-09, by clasohm
renamed int-prover.ML to intprover.ML,
1993-11-09, by clasohm
now forbids semicolons in the body of br, etc. No longer
1993-11-09, by lcp
Minor changes; addition of counit.ML
1993-11-08, by lcp
change of my address
1993-11-05, by nipkow
Added documenation of change_simp.
1993-11-05, by lcp
renamed co_inductive.ML to coinductive.ML
1993-11-04, by clasohm
renamed twos-compl.ML to twos_compl.ML
1993-11-04, by clasohm
renamed some files
1993-11-04, by clasohm
commented out install_pp for term, typ
1993-11-04, by wenzelm
added infix delsimps
1993-10-29, by nipkow
added function del_simps
1993-10-29, by nipkow
deletion of obsolete/private files; update of README
1993-10-28, by lcp
minor changes e.g. datatype_elims
1993-10-28, by lcp
now uses datatype_intrs and datatype_elims
1993-10-28, by lcp
updated version to October 93
1993-10-28, by lcp
no longer specifies "-h 15000". Instead $ISABELLECOMP should
1993-10-27, by lcp
corrected some spelling mistakes;
1993-10-26, by clasohm
added white-space;
1993-10-25, by wenzelm
added white-space;
1993-10-25, by wenzelm
removed a bug that occured when a path was specified for use_thy's parameter
1993-10-22, by clasohm
ZF/ex/tf,tf_fn: renamed the variable tf to f everywhere
1993-10-22, by lcp
renamed some files
1993-10-22, by clasohm
added -h 15000 for Poly/ML in Makefile,
1993-10-22, by clasohm
changes in Readthy:
1993-10-22, by clasohm
delete_file now has type string -> unit in both NJ and POLY,
1993-10-22, by clasohm
changes for new Readthy
1993-10-22, by clasohm
sample datatype defs now use datatype_intrs, datatype_elims
1993-10-22, by lcp
ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
1993-10-22, by lcp
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
1993-10-22, by lcp
goals/print_top,prepare_proof: now call \!print_goals_ref
1993-10-22, by lcp
Pure/drule/print_goals_ref: new, for Centaur interface
1993-10-21, by lcp
/NJ,POLY/delete_file: new
1993-10-21, by lcp
simpdata/basify: now calls new fastype_of
1993-10-21, by lcp
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
1993-10-21, by lcp
now calls new fastype_of in three places
1993-10-21, by lcp
Pure/Syntax/printer/is_prop: now calls fastype_of1
1993-10-21, by lcp
Pure/term/fastype_of1: renamed from fastype_of
1993-10-21, by lcp
renamed: S4.thy to s4.thy, S43.thy to s43.thy, T.thy to t.thy
1993-10-17, by clasohm
renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
1993-10-17, by clasohm
file_info now returns a string that does not contain the path/filename
1993-10-15, by clasohm
added parser.ML, install_pp.ML
1993-10-15, by wenzelm
ZF/ex/tf/tree,forest_unfold: streamlined the proofs
1993-10-15, by lcp
ZF/ind-syntax/refl_thin: new
1993-10-15, by lcp
classical/swap_res_tac: recoded to allow backtracking
1993-10-15, by lcp
Added gen_all to simpdata.ML.
1993-10-12, by nipkow
renamed ordinal.thy to ord.thy
1993-10-11, by clasohm
renamed ordinal.ML to ord.ML
1993-10-11, by clasohm
renamed ordinal.* to ord.*
1993-10-11, by clasohm
"The" now a binder, removed translation;
1993-10-11, by wenzelm
removed ndependent_tr (no longer needed, use _K);
1993-10-11, by wenzelm
*** empty log message ***
1993-10-11, by wenzelm
*** empty log message ***
1993-10-08, by wenzelm
fixed comment;
1993-10-08, by wenzelm
added parse rule for "<*>";
1993-10-08, by wenzelm
@List: replaced "args" by "is";
1993-10-08, by wenzelm
*** empty log message ***
1993-10-08, by wenzelm
added cons, rcons, last_elem, sort_strings, take_suffix;
1993-10-08, by wenzelm
added raise_type: string -> typ list -> term list -> 'a;
1993-10-08, by wenzelm
"The error/exception above ...": errorneous goal now quoted;
1993-10-08, by wenzelm
used ~: for "not in"
1993-10-07, by lcp
added ~: for "not in"
1993-10-07, by lcp
examples now use ~= for "not equals"
1993-10-07, by lcp
ifol.thy: added ~= for "not equals"
1993-10-07, by lcp
changed filenames to lower case name of theory the file contains
1993-10-06, by clasohm
rename list-fn to listfn
1993-10-06, by clasohm
changed "list-fn" to "listfn"
1993-10-06, by clasohm
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
1993-10-06, by lcp
Retrying yet again after network problems
1993-10-06, by lcp
Modification of examples for the new operators, < and le.
1993-10-05, by lcp
Retry of the previous commit (network outage)
1993-10-05, by lcp
Retry of the previous commit (network outage)
1993-10-05, by lcp
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
1993-10-05, by lcp
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
1993-10-05, by lcp
added functions that operate on filenames: split_filename (originally located
1993-10-05, by clasohm
replaced id by idt;
1993-10-04, by wenzelm
added parse rules for -> and *;
1993-10-04, by wenzelm
replaced id by idt;
1993-10-04, by wenzelm
Pure/Thy/syntax.ML
1993-10-04, by wenzelm
Pure/ROOT.ML
1993-10-04, by wenzelm
lots of internal cleaning and tuning;
1993-10-04, by wenzelm
asm_full_simp_tac now fails when applied to a state w/o subgoals.
1993-10-01, by nipkow
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-30, by lcp
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-30, by lcp
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-30, by lcp
Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10
1993-09-24, by lcp
Added ex_ex1I: new introduction rule for the EX! quantifier.
1993-09-24, by lcp
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
1993-09-24, by lcp
This commit should not have been necessary. For some reason, the previous
1993-09-21, by lcp
make-all now has set +e so that New Jersey runs will continue even if some
1993-09-20, by lcp
Installation of new simplfier. Previously appeared to set up the old
1993-09-20, by lcp
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
1993-09-17, by lcp
Installation of new simplifier for ZF. Deleted all congruence rules not
1993-09-17, by lcp
test commit
1993-09-17, by lcp
added header
1993-09-16, by nipkow
defined local addcongs
1993-09-16, by nipkow
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
1993-09-16, by clasohm
changed addcongs to addeqcongs in simplifier.ML
1993-09-16, by nipkow
Initial revision
1993-09-16, by clasohm
less
more
|
(0)
+480
+1000
+3000
+10000
+30000
tip