1997-04-04 wenzelm 1997-04-04 improved messages;
1997-04-04 wenzelm 1997-04-04 fixed diagnostic output of print modes;
1997-04-04 nipkow 1997-04-04 moved inj and surj from Set to Fun and Inv -> inv.
1997-04-04 nipkow 1997-04-04 Inv -> inv
1997-04-04 slotosch 1997-04-04 *** empty log message ***
1997-04-04 slotosch 1997-04-04 Added Example Quot CVS ----------------------------------------------------------------------
1997-04-04 slotosch 1997-04-04 Start Example
1997-04-04 nipkow 1997-04-04 inv -> inverse
1997-04-04 slotosch 1997-04-04 Example for higher order quotients: Fractionals
1997-04-04 slotosch 1997-04-04 (higher-order) quotient constructor quot, based on PER
1997-04-04 slotosch 1997-04-04 (partial) equivalecne relations. classes er<per
1997-04-04 nipkow 1997-04-04 Inv -> inv
1997-04-04 wenzelm 1997-04-04 added -b option (batch mode);
1997-04-04 nipkow 1997-04-04 renamed variable 'inv'
1997-04-04 wenzelm 1997-04-04 added Quot examples;
1997-04-04 wenzelm 1997-04-04 *** empty log message ***
1997-04-04 wenzelm 1997-04-04 Higher-order quotients.
1997-04-04 paulson 1997-04-04 Now calls blast_tac
1997-04-04 paulson 1997-04-04 Another blast_tac call
1997-04-04 paulson 1997-04-04 Simplified a proof
1997-04-04 paulson 1997-04-04 Re-organization of the order of haz rules
1997-04-04 paulson 1997-04-04 Calls Blast_tac. Tidied some proofs
1997-04-04 paulson 1997-04-04 Calls Blast_tac. Tidied some proofs
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-04-04 paulson 1997-04-04 Adds image_eqI instead of imageI, as the former is more general
1997-04-04 paulson 1997-04-04 Added blast.ML as a dependency
1997-04-04 paulson 1997-04-04 Now calls Blast_tac and has some hard examples (Halting Problem
1997-04-03 nipkow 1997-04-03 Only layout mods.
1997-04-03 nipkow 1997-04-03 Now: unit = {True}
1997-04-03 paulson 1997-04-03 Two extra commands shorten the proof time by 800 seconds...
1997-04-03 paulson 1997-04-03 More List and ListPair utilities
1997-04-03 paulson 1997-04-03 Now exports declConsts! Temporarily erased target signature to aid debugging
1997-04-03 paulson 1997-04-03 Declares overloading for if-and-only-if
1997-04-03 paulson 1997-04-03 Declares overloading for set-theoretic constants
1997-04-03 nipkow 1997-04-03 Removed (Unit) in Prod. Added test for ancestor Nat in datatype.
1997-04-02 wenzelm 1997-04-02 misc improvements;
1997-04-02 wenzelm 1997-04-02 changed signature of dummy goal from proto_pure to pure;
1997-04-02 paulson 1997-04-02 Converted to call blast_tac. Proves theorems in ZF.thy to make that theory usable again
1997-04-02 paulson 1997-04-02 Uses ZF.thy again, to make that theory usable
1997-04-02 paulson 1997-04-02 Mostly converted to blast_tac
1997-04-02 paulson 1997-04-02 Datatype declarations now require theory Datatype--NOT in quotes
1997-04-02 paulson 1997-04-02 Converted back from upair.thy to ZF.thy
1997-04-02 paulson 1997-04-02 Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
1997-04-02 paulson 1997-04-02 Now checks for existence of theory Inductive (Fixedpt was too small)
1997-04-02 paulson 1997-04-02 Now a non-trivial theory so that require_thy can find it
1997-04-02 paulson 1997-04-02 DEEPEN now takes an upper bound for terminating searches
1997-04-02 paulson 1997-04-02 New DEEPEN allows giving an upper bound for deepen_tac
1997-04-02 paulson 1997-04-02 Now builds blast_tac
1997-04-02 paulson 1997-04-02 Now loads blast.ML
1997-04-02 paulson 1997-04-02 ZF.thy is again usable
1997-04-02 wenzelm 1997-04-02 The isabelle-0 encoding table.
1997-04-02 paulson 1997-04-02 Made the error message more explicit
1997-04-02 paulson 1997-04-02 Now declares Basis Library version of type option Also function mapPartial
1997-04-02 paulson 1997-04-02 Replaced Best_tac by the one rule needed for the proof
1997-04-02 paulson 1997-04-02 Installation of blast_tac
1997-04-02 paulson 1997-04-02 Now tests for essential ancestors (Lfp or Gfp)
1997-04-02 paulson 1997-04-02 Re-ordering of rules to assist blast_tac Powerset rules must not be the most recent
1997-04-02 paulson 1997-04-02 Now loads blast_tac
1997-04-02 paulson 1997-04-02 Reorganization of how classical rules are installed
1997-04-02 paulson 1997-04-02 Now calls require_thy to ensure ancestors are present