isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

Changed some fast_tac to blast_tac
1997-04-10, by paulson
Added trace output and replaced fast_tac set_cs by Fast_tac.
1997-04-10, by nipkow
replaced 'addwrapper' and 'addWrapper' by correct 'compwrapper' and 'compWrapper'
1997-04-09, by oheimb
Thorough update.
1997-04-09, by nipkow
Using Blast_tac
1997-04-09, by paulson
Control over excessive branching by applying a log2 penalty
1997-04-09, by paulson
Explicit depth bounds seem necessary
1997-04-09, by paulson
Using Blast_tac
1997-04-09, by paulson
Dependency on Provers/nat_transitive
1997-04-09, by paulson
Couldn't solve n < n+1 because of missing -1
1997-04-08, by nipkow
Dep. on Provers/nat_transitive
1997-04-08, by nipkow
added -t (run tests) option;
1997-04-07, by wenzelm
added -g, -h options;
1997-04-04, by wenzelm
tuned xdvi invocation;
1997-04-04, by wenzelm
replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;
1997-04-04, by wenzelm
improved messages;
1997-04-04, by wenzelm
fixed diagnostic output of print modes;
1997-04-04, by wenzelm
moved inj and surj from Set to Fun and Inv -> inv.
1997-04-04, by nipkow
Inv -> inv
1997-04-04, by nipkow
*** empty log message ***
1997-04-04, by slotosch
Added Example Quot
1997-04-04, by slotosch
Start Example
1997-04-04, by slotosch
inv -> inverse
1997-04-04, by nipkow
Example for higher order quotients: Fractionals
1997-04-04, by slotosch
(higher-order) quotient constructor quot, based on PER
1997-04-04, by slotosch
(partial) equivalecne relations. classes er<per
1997-04-04, by slotosch
Inv -> inv
1997-04-04, by nipkow
added -b option (batch mode);
1997-04-04, by wenzelm
renamed variable 'inv'
1997-04-04, by nipkow
added Quot examples;
1997-04-04, by wenzelm
*** empty log message ***
1997-04-04, by wenzelm
Higher-order quotients.
1997-04-04, by wenzelm
Now calls blast_tac
1997-04-04, by paulson
Another blast_tac call
1997-04-04, by paulson
Simplified a proof
1997-04-04, by paulson
Re-organization of the order of haz rules
1997-04-04, by paulson
Calls Blast_tac. Tidied some proofs
1997-04-04, by paulson
Calls Blast_tac. Tidied some proofs
1997-04-04, by paulson
Calls Blast_tac
1997-04-04, by paulson
Adds image_eqI instead of imageI, as the former is more general
1997-04-04, by paulson
Added blast.ML as a dependency
1997-04-04, by paulson
Now calls Blast_tac and has some hard examples (Halting Problem
1997-04-04, by paulson
Only layout mods.
1997-04-03, by nipkow
Now: unit = {True}
1997-04-03, by nipkow
Two extra commands shorten the proof time by 800 seconds...
1997-04-03, by paulson
More List and ListPair utilities
1997-04-03, by paulson
Now exports declConsts!
1997-04-03, by paulson
Declares overloading for if-and-only-if
1997-04-03, by paulson
Declares overloading for set-theoretic constants
1997-04-03, by paulson
Removed (Unit) in Prod.
1997-04-03, by nipkow
misc improvements;
1997-04-02, by wenzelm
changed signature of dummy goal from proto_pure to pure;
1997-04-02, by wenzelm
Converted to call blast_tac.
1997-04-02, by paulson
Uses ZF.thy again, to make that theory usable
1997-04-02, by paulson
Mostly converted to blast_tac
1997-04-02, by paulson
Datatype declarations now require theory Datatype--NOT in quotes
1997-04-02, by paulson
Converted back from upair.thy to ZF.thy
1997-04-02, by paulson
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
1997-04-02, by paulson
Now checks for existence of theory Inductive (Fixedpt was too small)
1997-04-02, by paulson
Now a non-trivial theory so that require_thy can find it
1997-04-02, by paulson

less more | (0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle