isabelle: Graph

(temporary remove, forgotten the -b flag...)
2005-06-04, by haftmann
major reorganization and cleanup;
2005-06-04, by wenzelm
added new website
2005-06-04, by haftmann
added explicit dependency on Fix theory
2005-06-04, by huffman
add keywords fixrec and fixpat for HOLCF fixrec package
2005-06-04, by huffman
fix imports
2005-06-04, by huffman
use fixrec_package.ML
2005-06-04, by huffman
import Fix is unnecessary
2005-06-04, by huffman
added fixrec_package.ML
2005-06-04, by huffman
implementation of fixrec package
2005-06-04, by huffman
shrink session graph so it fits on a page
2005-06-04, by huffman
Domain package generates match functions for new datatypes, for use with the fixrec package
2005-06-04, by huffman
add dependency on Fixrec.thy
2005-06-04, by huffman
add Fixrec.thy
2005-06-04, by huffman
New theory with lemmas for the fixrec package
2005-06-04, by huffman
changed variable name in monofun_cfun_arg
2005-06-03, by huffman
fixed renamed theorems
2005-06-03, by huffman
fixed some renamed theorems
2005-06-03, by huffman
renamed defined lemmas
2005-06-03, by huffman
renamed variable in cont2cont_app
2005-06-03, by huffman
changed to use new contlubI, etc.
2005-06-03, by huffman
cleaned up proof of cont_Ifix
2005-06-03, by huffman
replaced cont with cont_def
2005-06-03, by huffman
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
2005-06-03, by huffman
changed to use new contI; renamed strict, defined, and inject lemmas
2005-06-03, by huffman
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
2005-06-03, by huffman
removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
2005-06-03, by huffman
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency
2005-06-03, by huffman
changed to work with new contlubE rule
2005-06-03, by huffman
renamed FunCpo to Ffun
2005-06-03, by huffman
renamed to Ffun (full function space)
2005-06-03, by huffman
renamed theorems monofun, contlub, cont to monofun_def, etc.; changed intro/elim rules for these predicates into more useful rule_format; removed all MF2 lemmas (Pcpo.thy has more general versions now); cleaned up many proofs.
2005-06-03, by huffman
added theorem ch2ch_lub
2005-06-03, by huffman
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
2005-06-03, by huffman
added theorems diag_lub and ex_lub
2005-06-03, by huffman
fixed a typo in the gfp interpreter
2005-06-03, by webertj
no longer emits literals for type class HOL.type; also minor tidying
2005-06-03, by paulson
Integrates cycle detection in definitions with finalconsts
2005-06-03, by obua
tuned msgs;
2005-06-02, by wenzelm
html_syms table;
2005-06-02, by wenzelm
tuned;
2005-06-02, by wenzelm
Output.no_warnings;
2005-06-02, by wenzelm
tuned comment;
2005-06-02, by wenzelm
exists: made non-strict;
2005-06-02, by wenzelm
added no_warnings;
2005-06-02, by wenzelm
Sign.restore_naming;
2005-06-02, by wenzelm
replaced set_naming by restore_naming;
2005-06-02, by wenzelm
replaced foldl_string by fold_string;
2005-06-02, by wenzelm
renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
2005-06-02, by wenzelm
renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
2005-06-02, by wenzelm
Added time lime (60 secs) to Spass calls.
2005-06-02, by quigley
renamed "constrains" to "safety" to avoid keyword clash
2005-06-02, by paulson
renamed "constrains" to "safety" to avoid keyword clash
2005-06-02, by paulson
swap declaration of thm/axm names to accomodate change in name space
2005-06-02, by wenzelm
tuned;
2005-06-02, by wenzelm
Theory.restore_naming;
2005-06-02, by wenzelm
header;
2005-06-02, by wenzelm
reduced timeout, send logs also when test taking too long
2005-06-02, by kleing
Preliminary version of defs.ML that does not check final consts.
2005-06-01, by obua
*** empty log message ***
2005-06-01, by nipkow
tuned
2005-06-01, by nipkow
ordering for the ordinals
2005-06-01, by paulson
clausification bug fix
2005-06-01, by paulson
small tweaks; also now write_out_clasimp takes the current theory as argument
2005-06-01, by paulson
remove CVS id from *.sty latex styles
2005-06-01, by haftmann
remove CVS id from *.sty latex styles
2005-06-01, by haftmann
Locales: new element constrains, parameter renaming with syntax,
2005-06-01, by ballarin
Locales: new element constrains, parameter renaming with syntax,
2005-06-01, by ballarin
renamed premise* to prem
2005-06-01, by haftmann
some refinements
2005-06-01, by haftmann
concl antiqutations
2005-06-01, by haftmann
*** empty log message ***
2005-06-01, by nipkow
improved *.sty handling
2005-06-01, by haftmann
improved *.sty handling
2005-06-01, by haftmann
improved *.sty handling
2005-06-01, by haftmann
added premise<i>
2005-06-01, by nipkow
added dependency
2005-06-01, by nipkow
Removed final_consts from theory data. Now const_deps deals with final
2005-05-31, by obua
minor tidying and sml/nj compatibility
2005-05-31, by paulson
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
2005-05-31, by quigley
fixed sectioning
2005-05-31, by nipkow
\nexists
2005-05-31, by nipkow
\nexists und premsise1 .. 9
2005-05-31, by nipkow
no_tac;
2005-05-31, by wenzelm
ML Pure: name spaces have been refined;
2005-05-31, by wenzelm
moved is_ident to General/symbol.ML;
2005-05-31, by wenzelm
Theory.restore_naming;
2005-05-31, by wenzelm
make: T option -- actually remove undefined cases;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
method_cases: RuleCases.T option;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
improved naming of complex theorems in presentation;
2005-05-31, by wenzelm
added short_names, unique_names options;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
added symbol scanner;
2005-05-31, by wenzelm
remove(_multi): generalized type;
2005-05-31, by wenzelm
added is_ident (from Syntax/lexicon.ML);
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
tuned arrangement of structures;
2005-05-31, by wenzelm
added eq_thms;
2005-05-31, by wenzelm
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
tuned msg;
2005-05-31, by wenzelm
added nth_prem;
2005-05-31, by wenzelm
export filter;
2005-05-31, by wenzelm
Sign.declare_name replaces NameSpace.extend;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
fixed outer syntax: allow type_args with parentheses;
2005-05-31, by wenzelm
proper use of Sign.full_name;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
Theory.restore_naming;
2005-05-31, by wenzelm
renamed cond_extern to extern;
2005-05-31, by wenzelm
tuned;
2005-05-31, by wenzelm
antiquotations: added options short_names, unique_names;
2005-05-31, by wenzelm
improved naming of complex theorems in presentation;
2005-05-31, by wenzelm
removed;
2005-05-31, by wenzelm
tuned;
2005-05-31, by wenzelm
tuned;
2005-05-31, by wenzelm
tuned;
2005-05-31, by wenzelm
tuned;
2005-05-30, by wenzelm
Infinite chains in definitions are now detected, too.
2005-05-30, by obua
typo
2005-05-30, by kleing
updated para on searching
2005-05-30, by kleing
added \nexists
2005-05-30, by nipkow
Removes an inconsistent definition from Library.thy ,
2005-05-29, by obua
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
2005-05-29, by obua
make COPYRIGHT file available for web page
2005-05-29, by kleing
path /home/stud doesn't exist on macbroy33 (only /usr/stud)
2005-05-28, by kleing
SML/NJ compatibility.
2005-05-27, by ballarin
Typo.
2005-05-27, by ballarin
Deleted old code.
2005-05-27, by ballarin
Locale expressions: rename with optional mixfix syntax.
2005-05-27, by ballarin
Add back rudely removed and popular -X option.
2005-05-27, by aspinall
Now uses File.write and File.append
2005-05-27, by paulson
removed obsolete theorems
2005-05-27, by huffman
use TypedefPcpo for all class instances
2005-05-27, by huffman
log more failure types
2005-05-27, by kleing
added lemmas monofun_lub_fun and cont_lub_fun
2005-05-27, by huffman
put global isatest settings in one file, sourced by the other scripts
2005-05-27, by kleing
Use TypedefPcpo theorem for po instance
2005-05-27, by huffman
use thelub_const lemma
2005-05-27, by huffman
added lemma thelub_const
2005-05-27, by huffman
further tweaks to the SPASS setup
2005-05-26, by paulson
goodby to modUnix
2005-05-26, by paulson
trying to set up portable calling sequences for SPASS and tptp2X
2005-05-26, by paulson
cleaned up select_match
2005-05-26, by kleing
Narrower version of the Proof General's head; removal of the alternative icon and environment
2005-05-26, by paulson
Narrower version of the Proof General's head
2005-05-26, by paulson
rewrote continuous isomorphism section, cleaned up
2005-05-26, by huffman
cleaned up, added UU_app and less_funI, removed some obsolete stuff
2005-05-26, by huffman
added defaultsort declaration, moved cpair_less to Cprod.thy
2005-05-26, by huffman
added defaultsort declaration
2005-05-26, by huffman
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
2005-05-26, by huffman
removed dependence on Cfun.thy
2005-05-26, by huffman
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
2005-05-26, by huffman
new Brouwer ordinal example
2005-05-25, by paulson
more cleanup
2005-05-25, by kleing
tuned thm_style section
2005-05-25, by kleing
added ? explanations
2005-05-25, by nipkow
renamed search criterion 'rewrite' to 'simp'
2005-05-25, by kleing
SML/NJ compatibility
2005-05-25, by paulson
new environments for Proof General notes
2005-05-25, by paulson
removed obsolete findI, findE, findEs
2005-05-25, by kleing
removed LICENCE note -- everything is subject to Isabelle licence as
2005-05-25, by wenzelm
*** empty log message ***
2005-05-25, by nipkow
grammar
2005-05-25, by nipkow
shorted proof that lift is chfin
2005-05-25, by huffman
Removed shell variables. Now uses isatool getenv -b SPASS_HOME.
2005-05-25, by quigley
Generic version of spassshell. Add SPASS_HOME to .bashrc so that shell script can find it.
2005-05-24, by quigley
ML_idf antiquotation
2005-05-24, by haftmann
oracle example converted to Isar
2005-05-24, by paulson
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
2005-05-24, by paulson
A new structure and reduced indentation
2005-05-24, by paulson
Simplified version of strict sum theory, using TypedefPcpo
2005-05-24, by huffman
Simplified version of strict product theory, using TypedefPcpo
2005-05-24, by huffman
New theory for defining subtypes of pcpos
2005-05-24, by huffman
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
2005-05-24, by huffman
Moved admissibility definitions and lemmas to a separate theory
2005-05-24, by huffman
moved continuity simproc to Cfun.thy
2005-05-23, by huffman
moved continuity simproc to Cont.thy
2005-05-23, by huffman
moved theorem cont2cont_CF1L_rev2 to Cont.thy
2005-05-23, by huffman
tuned setsum rewrites
2005-05-23, by nipkow
* Pure/Syntax: In schematic variable names, *any* symbol following
2005-05-23, by wenzelm
interpreters for lfp/gfp added
2005-05-23, by webertj
obsolete;
2005-05-23, by wenzelm
spassshell and testout.py are used to filter the proof part out of SPASS's
2005-05-23, by quigley
tuned pretty_sg;
2005-05-23, by wenzelm
node_trans: revert to original transaction code (pre 1.54);
2005-05-23, by wenzelm
use: not a theory command!
2005-05-23, by wenzelm
converted back from 0..< to <.
2005-05-23, by nipkow
added email
2005-05-23, by haftmann
tuned trace info (depth)
2005-05-23, by nipkow
simplifier trace info; Suc-intervals
2005-05-23, by nipkow
some adaptions
2005-05-23, by haftmann
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
2005-05-23, by quigley
tuned;
2005-05-22, by wenzelm
string FindTheorems.criterion;
2005-05-22, by wenzelm
added read_criterion/pretty_criterion;
2005-05-22, by wenzelm
added show_dummy_patterns;
2005-05-22, by wenzelm
updated;
2005-05-22, by wenzelm
Retrieve theorems from proof context -- improved version of
2005-05-22, by wenzelm
added Pure/simplifier.ML, Pure/Isar/find_theorems.ML;
2005-05-22, by wenzelm
moved everything related to thms_containing to find_theorems.ML;
2005-05-22, by wenzelm
added reserved;
2005-05-22, by wenzelm
added ident_with;
2005-05-22, by wenzelm
fold ProofContext.declare_term;
2005-05-22, by wenzelm
added 'print_simpset';
2005-05-22, by wenzelm
added print_simpset;
2005-05-22, by wenzelm
added find_theorems.ML, ../simplifier.ML;
2005-05-22, by wenzelm
tuned terms_of_tpairs;
2005-05-22, by wenzelm
added string_of_thmref, selections, fact_index_of, valid_thms;
2005-05-22, by wenzelm
FindTheorems.print_theorems;
2005-05-22, by wenzelm
findI/Es/E: adapted to FindTheorems.find_XXX, results use thmref instead of string;
2005-05-22, by wenzelm
major tuning;
2005-05-22, by wenzelm
Simplifier already setup in Pure;
2005-05-22, by wenzelm
tuned antiquotations;
2005-05-22, by wenzelm
tuned thms_containing;
2005-05-22, by wenzelm
tuned;
2005-05-22, by wenzelm
moved to Pure;
2005-05-22, by wenzelm
moved here from Provers;
2005-05-22, by wenzelm
removed find_rewrites (superceded by improved thms_containing);
2005-05-22, by wenzelm
bug fixes for clause form transformation
2005-05-20, by paulson
converted some problems to Isar format
2005-05-20, by paulson
subst again
2005-05-19, by nipkow
Skolemization of simprules and classical rules
2005-05-19, by paulson
pcpo instance for type unit
2005-05-19, by huffman
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
2005-05-19, by dixon
shortened proof of adm_disj
2005-05-18, by huffman
cleaned up and shortened some proofs
2005-05-18, by huffman
lucas - fixed subst in assumptions to count redexes from left to right.
2005-05-18, by dixon
removed update_node, which is just an instance of map_node;
2005-05-18, by wenzelm
tuned;
2005-05-18, by wenzelm
updated;
2005-05-18, by wenzelm
searching for combination of criteria (intro, elim, dest, name, pattern)
2005-05-18, by kleing
made para on searching more readable
2005-05-18, by kleing
new cnf function taking Skolemization theorems as an extra argument
2005-05-18, by paulson
consolidation and simplification
2005-05-18, by paulson
documented new thms_containing ('rewrites' still missing)
2005-05-18, by kleing
documented new subst
2005-05-18, by nipkow
proper Id line;
2005-05-17, by wenzelm
updated;
2005-05-17, by wenzelm
var_or_skolem: always print question mark for vars stemming from skolems;
2005-05-17, by wenzelm
added read_variable: optional question mark on input;
2005-05-17, by wenzelm
substantial tuning -- adapted to common conventions;
2005-05-17, by wenzelm
re-init ml_prompts after loop termination;
2005-05-17, by wenzelm
renamed show_var_qmarks to show_question_marks;
2005-05-17, by wenzelm
Syntax.read_variable;
2005-05-17, by wenzelm
renamed show_var_qmarks to show_question_marks;
2005-05-17, by wenzelm
renamed show_var_qmarks to show_question_marks;
2005-05-17, by wenzelm
updated;
2005-05-17, by wenzelm
renamed show_var_qmarks to show_question_marks;
2005-05-17, by wenzelm
removed ISAMODE settings;
2005-05-17, by wenzelm
no longer support isa-FOO interface;
2005-05-17, by wenzelm
no longer support isa-FOO interface;
2005-05-17, by wenzelm