isabelle: Graph

updated;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
more contributions;
2005-09-20, by wenzelm
tuned headers;
2005-09-20, by wenzelm
tuned header;
2005-09-20, by wenzelm
use "ML-Systems/smlnj-basis-compat.ML" *after* Interrupt;
2005-09-20, by wenzelm
fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
2005-09-20, by wenzelm
bugfix in "zchaff_with_proofs"
2005-09-20, by webertj
fixed recursive-looking declaration
2005-09-20, by paulson
tidying, and support for axclass/classrel clauses
2005-09-20, by paulson
fixed syntax for sml/nj
2005-09-20, by paulson
undone the previous change: show_hyps not supported anymore
2005-09-20, by webertj
pointers to src/HOL/Tools/sat_solver.ML added in comments
2005-09-20, by webertj
introduced AList module in favor of assoc etc.
2005-09-20, by haftmann
new menu item show-sort-hypotheses to toggle show_hyps
2005-09-20, by webertj
HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
HOL-ex: Library/Commutative_Ring.thy;
2005-09-20, by wenzelm
moved Tools/comm_ring.ML to Library;
2005-09-20, by wenzelm
added Commutative_Ring (from Main HOL);
2005-09-20, by wenzelm
Simplifier.inherit_bounds;
2005-09-20, by wenzelm
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
2005-09-20, by wenzelm
get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
2005-09-20, by wenzelm
removed obsolete thms_containing;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
tuned simprocs;
2005-09-20, by wenzelm
removed Commutative_Ring hacks;
2005-09-20, by wenzelm
tuned theory dependencies;
2005-09-20, by wenzelm
removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
Chinese Unicode example;
2005-09-20, by wenzelm
tuned proofs;
2005-09-20, by wenzelm
The simpset of the actual theory is take, in order to handle rings defined after the method
2005-09-20, by chaieb
further tidying; killing of old Watcher loops
2005-09-20, by paulson
added a number of lemmas
2005-09-20, by nipkow
uniform handling of interrupts
2005-09-20, by paulson
algebra method added.
2005-09-20, by chaieb
improved eq_fst and eq_snd, removed some deprecated stuff
2005-09-20, by haftmann
added make and find
2005-09-20, by haftmann
slight adaptions to library changes
2005-09-20, by haftmann
infix operator precedence
2005-09-20, by haftmann
using curried Inttab.update_new function now
2005-09-20, by webertj
SAT solver interface modified to support proofs of unsatisfiability
2005-09-19, by webertj
shrink: compress terms and types;
2005-09-19, by wenzelm
added String.isSuffix;
2005-09-19, by wenzelm
maybe the last bug fix (sigh)?
2005-09-19, by obua
Removed superfluous HOL/Matrix/cplex/ROOT.ML.
2005-09-19, by obua
further simplification of the Isabelle-ATP linkup
2005-09-19, by paulson
added make function
2005-09-19, by haftmann
removed some deprecated assocation list functions
2005-09-19, by haftmann
introduced AList module
2005-09-19, by haftmann
simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-19, by paulson
update usage message
2005-09-19, by kleing
obsolete;
2005-09-19, by wenzelm
converted to Isar theory format;
2005-09-18, by wenzelm
converted to Isar theory format;
2005-09-18, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
moved quick_and_dirty to Pure/ROOT.ML;
2005-09-17, by wenzelm
pretty_thm_aux: ora masked by quick_and_dirty;
2005-09-17, by wenzelm
added quick_and_dirty (from Isar/skip_proofs.ML);
2005-09-17, by wenzelm
manually generated from Isabelle/HOLCF/IOA/Complex/Import;
2005-09-17, by wenzelm
tuned document;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
2005-09-17, by wenzelm
tuned comments;
2005-09-17, by wenzelm
pretty_thm_aux: aconv hyps;
2005-09-17, by wenzelm
removed obsolete BasisLibrary;
2005-09-17, by wenzelm
Hebrew: HTML.with_charset;
2005-09-17, by wenzelm
removed obsolete BasisLibrary;
2005-09-17, by wenzelm
added quickcheck_params (from Main.thy);
2005-09-17, by wenzelm
removed spurious PolyML.exception_trace;
2005-09-17, by wenzelm
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
2005-09-17, by wenzelm
minor cleanup, moved stuff in its proper place;
2005-09-17, by wenzelm
generate: added HOL-Complex-Generate-HOLLight;
2005-09-17, by wenzelm
added code generator setup (from Main.thy);
2005-09-17, by wenzelm
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
2005-09-17, by wenzelm
HTML.with_charset;
2005-09-17, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
tuned document;
2005-09-17, by wenzelm
obsolete;
2005-09-17, by wenzelm
plain test session, includes example;
2005-09-17, by wenzelm
theory_to_proof: check theory of initial proof state, which must not be changed;
2005-09-17, by wenzelm
added auto_fix (from proof.ML);
2005-09-17, by wenzelm
export put_facts;
2005-09-17, by wenzelm
interpretation: use goal commands without target -- no storing of results;
2005-09-17, by wenzelm
theorem(_i): empty target;
2005-09-17, by wenzelm
pretty_thm_aux: observe asms context;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
Cube: converted to Isar, use locales;
2005-09-17, by wenzelm
1) mapped .. and == constants
2005-09-17, by obua
use interpretation command
2005-09-17, by huffman
add HOLCF entries for pcpodef, cont_proc, fixrec;
2005-09-16, by huffman
converted to Isar theory format;
2005-09-16, by wenzelm
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
2005-09-16, by obua
add header
2005-09-16, by huffman
tuned
2005-09-16, by ballarin
interpretation uses primitive goal interface
2005-09-16, by ballarin
tuned
2005-09-16, by ballarin
PARTIAL conversion to Vampire8
2005-09-16, by paulson
catching exception Io
2005-09-16, by paulson
rearranged
2005-09-16, by huffman
use mem operator
2005-09-16, by huffman
fix names in hypreal_arith.ML
2005-09-16, by huffman
merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
2005-09-15, by huffman
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
2005-09-15, by huffman
add header
2005-09-15, by huffman
The SMLNJ Problem fixed...
2005-09-15, by chaieb
getting it work for SMLNJ
2005-09-15, by chaieb
* Improved efficiency of the Simplifier etc.;
2005-09-15, by wenzelm
incorporated into NEWS;
2005-09-15, by wenzelm
incorporated HOL/Hyperreal/CHANGES;
2005-09-15, by wenzelm
massive tidy-up and simplification
2005-09-15, by paulson
moving Commutative_Ring to the correct theory
2005-09-15, by paulson
comment
2005-09-15, by paulson
poly -doDisplay;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
fixed type;
2005-09-15, by wenzelm
fixed ML;
2005-09-15, by wenzelm
The Hebrew Alef-Bet -- Unicode example;
2005-09-15, by wenzelm
added Hebrew.thy;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
fixed document;
2005-09-15, by wenzelm
added HOL/ex/Hebrew.thy;
2005-09-15, by wenzelm
obsolete;
2005-09-15, by wenzelm
command 'thms_containing' has been discontinued in favour of 'find_theorems';
2005-09-15, by wenzelm
Revert previous attribute name change, problem can be avoided in JAXB.
2005-09-15, by aspinall
forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;
2005-09-15, by wenzelm
extend: NameSpace.default_naming;
2005-09-15, by wenzelm
the experimental tagging system, and the usual tidying
2005-09-15, by paulson
Change PGIP attribute name class->messageclass to avoid Java keyword clash.
2005-09-15, by aspinall
AList, the_*
2005-09-15, by haftmann
fixed type annotation
2005-09-15, by haftmann
added gen_list to Pretty module
2005-09-15, by haftmann
@{term [source] ...} in subsections probably more robust;
2005-09-14, by wenzelm
tuned;
2005-09-14, by wenzelm
hide: added option '(open)';
2005-09-14, by wenzelm
imports Commutative_Ring instead of Main, since the latter hides our names;
2005-09-14, by wenzelm
hide the rather generic names used in theory Commutative_Ring;
2005-09-14, by wenzelm
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
2005-09-14, by wenzelm
... prem19
2005-09-14, by schirmer
added prem10 - prem19
2005-09-14, by schirmer
removed syntax fun_map_comp;
2005-09-14, by schirmer
Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
2005-09-14, by chaieb
Method comm_ring for proving equalities in commutative rings.
2005-09-14, by wenzelm
tuned headers etc.;
2005-09-14, by wenzelm
fixed some ML names;
2005-09-14, by wenzelm
imports Commutative_Ring;
2005-09-14, by wenzelm
HOL: method comm_ring;
2005-09-14, by wenzelm
tuned;
2005-09-14, by wenzelm
no longer prefer xemacs, which fails more often than GNU emacs;
2005-09-14, by wenzelm
Bernhard Haeupler: comm_ring;
2005-09-14, by wenzelm
tactic and the rest eliminated, just the theory....
2005-09-14, by chaieb
use was wrong...
2005-09-14, by chaieb
Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
2005-09-14, by obua
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
2005-09-14, by chaieb
introduced AList.lookup
2005-09-14, by haftmann
correct E brackets
2005-09-14, by paulson
nice names for more infix operators
2005-09-14, by paulson
introduces AList.lookup
2005-09-14, by haftmann
removed duplicated lemmas; convert more proofs to transfer principle
2005-09-14, by huffman
add theorem chain_const
2005-09-13, by huffman
tuned;
2005-09-13, by wenzelm
global quick_and_dirty;
2005-09-13, by wenzelm
Printing of Isar proof elements etc.
2005-09-13, by wenzelm
Non-empty stacks.
2005-09-13, by wenzelm
IsarThy.begin_theory;
2005-09-13, by wenzelm
export ml_exts;
2005-09-13, by wenzelm
begin_theory: tuned interface, check uses;
2005-09-13, by wenzelm
replaced TRANSLATION_FAIL by EXCEPTION;
2005-09-13, by wenzelm
added three_buffersN, print3;
2005-09-13, by wenzelm
load before proof.ML;
2005-09-13, by wenzelm
added simple;
2005-09-13, by wenzelm
added add_view, export_view (supercedes adhoc view arguments);
2005-09-13, by wenzelm
major cleanup of interfaces and implementation;
2005-09-13, by wenzelm
added name_facts;
2005-09-13, by wenzelm
tuned Isar proof elements;
2005-09-13, by wenzelm
added cheating, sorry_text (from skip_proofs.ML);
2005-09-13, by wenzelm
load late, after proof.ML;
2005-09-13, by wenzelm
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
2005-09-13, by wenzelm
cleanup parsers and interfaces;
2005-09-13, by wenzelm
Proof.get_thmss;
2005-09-13, by wenzelm
tuned;
2005-09-13, by wenzelm
more self-contained proof elements (material from isar_thy.ML);
2005-09-13, by wenzelm
added cases, rule_contextN;
2005-09-13, by wenzelm
load locale.ML late (after proof.ML);
2005-09-13, by wenzelm
added maps, map_list, lift, lifts;
2005-09-13, by wenzelm
added stack.ML;
2005-09-13, by wenzelm
added simple_fact;
2005-09-13, by wenzelm
Seq.maps;
2005-09-13, by wenzelm
added hide_names(_i) (from isar_thy.ML);
2005-09-13, by wenzelm
added generic_setup, add_oracle (from isar_thy.ML);
2005-09-13, by wenzelm
added exception EXCEPTION of exn * string;
2005-09-13, by wenzelm
replaced DATA_FAIL by EXCEPTION;
2005-09-13, by wenzelm
tuned Isar interfaces;
2005-09-13, by wenzelm
added General/stack.ML, Isar/proof_display.ML;
2005-09-13, by wenzelm
the_list (cf. Pure/library.ML);
2005-09-13, by wenzelm
tuned IsarThy.theorem_i;
2005-09-13, by wenzelm
fixed INST: has same semantic now as INST_TYPE for repetitions
2005-09-13, by obua
list of constants and theorems whose names have been changed or merged
2005-09-12, by huffman
add header
2005-09-12, by huffman
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-12, by huffman
updated to work with latest HOL-Complex
2005-09-12, by huffman
add file Hyperreal/transfer.ML
2005-09-12, by huffman
new implementation of transfer principle
2005-09-12, by huffman
removed clutter
2005-09-12, by obua
name conflict with global itrev resolved
2005-09-12, by nipkow
dealt with name clash with List.itrev
2005-09-12, by nipkow
introduced new-style AList operations
2005-09-12, by haftmann
introduced internal function hthm2thm
2005-09-12, by obua
1) Added target HOL-Complex-Generate-HOLLight
2005-09-12, by obua
Added HOLLight support to importer.
2005-09-12, by obua
added interact flag to control mode of excursions;
2005-09-12, by wenzelm
excursion: interactive if debug;
2005-09-11, by wenzelm
updated to work with new HOL-Complex version
2005-09-09, by huffman
starfun, starset, and other functions on NS types are now polymorphic;
2005-09-09, by huffman
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-09, by paulson
fixed printing of locales
2005-09-09, by ballarin
consolidation of duplicate code in Isabelle-ATP linkup
2005-09-08, by paulson
introduces some modern-style AList operations
2005-09-08, by haftmann
added the_list, the_default
2005-09-08, by haftmann
yet more tidying of Isabelle-ATP link
2005-09-08, by paulson
converted to Isar theory format;
2005-09-07, by wenzelm
converted to Isar theory format;
2005-09-07, by wenzelm
converted to Isar theory format;
2005-09-07, by wenzelm
removed TLA/Inc/Pcount.thy;
2005-09-07, by wenzelm
elimination of watcher.sig
2005-09-07, by paulson
Progress on eprover linkup, also massive tidying
2005-09-07, by paulson
axioms now included in tptp files, no /bin/cat and various tidying
2005-09-07, by paulson
consolidation of watcher.ML and watcher.sig
2005-09-07, by paulson
generalized types more
2005-09-07, by huffman
generalized types
2005-09-07, by huffman
added theorem hypreal_inverse2
2005-09-07, by huffman
replace type hcomplex with complex star
2005-09-07, by huffman
replace type hypnat with nat star
2005-09-07, by huffman
replace type hypreal with real star
2005-09-06, by huffman
add Hyperreal dependencies
2005-09-06, by huffman