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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
Updated: 01Mar96 when functional strictified, copy_def based on when_def
19960403, by oheimb
Introduced Times and SIGMA.
19960403, by nipkow
*** empty log message ***
19960403, by oheimb
Plugged some more loopholes with nodup_Vars.
19960403, by nipkow
Simplified proof of tiling_UnI
19960329, by paulson
Binary integers and their numeric syntax
19960329, by paulson
new lemma for mutilated chess board
19960329, by paulson
Simplified proof of tiling_UnI
19960329, by paulson
Mended indentation
19960329, by paulson
Added functions pr_latex and printgoal_latex which
19960328, by berghofe
Optimized type inference (avoids chains of
19960328, by berghofe
Moved even/odd lemmas from ex/Mutil to Arith
19960328, by paulson
Translations for 1 and 2 moved from Hoare/Examples.thy to Nat.thy
19960328, by paulson
Alternative proof removes dependence upon AC
19960328, by paulson
Ran expandshort
19960328, by paulson
New theorem Finite_imp_succ_cardinal_Diff
19960328, by paulson
New mutilated checkerboard example
19960327, by paulson
Added Mutil to ex targets
19960327, by paulson
Now use _irrefl instead of _anti_refl
19960327, by paulson
Library changes for mutilated checkerboard
19960327, by paulson
Simplified proofs, esp. for new ZF_ss
19960326, by paulson
Moved some proofs to Cardinal.ML; simplified others
19960326, by paulson
Moved some proofs to FOL/IFOL.ML
19960326, by paulson
Rewriting changes due to new arith_ss
19960326, by paulson
Now loads Mutil example
19960326, by paulson
Added new rewrite rules about cons and succ
19960326, by paulson
New results from AC/Cardinal_aux.ML
19960326, by paulson
Updated comments
19960326, by paulson
New lemmas for Mutilated Checkerboard
19960326, by paulson
Added two of KGs rules
19960326, by paulson
New example file: Mutil
19960326, by paulson
New example: mutilated checkerboard
19960326, by paulson
added converse_converse
19960325, by nipkow
replaced "rules" by "primrec"
19960325, by nipkow
moved init_data to new public function set_current_thy
19960324, by clasohm
fixed incompatibility of add_to_parents with SML109's new Io exceptions
19960322, by clasohm
Changes required by removal of the theory argument of Theorem
19960321, by paulson
Examples call gocls to make goal clauses
19960321, by paulson
Now labels the Horn and goal clauses to make the proof
19960321, by paulson
For the new version of name_thm. Now the same theorem
19960321, by paulson
name_thm no longer takes a theory argument, as the
19960321, by paulson
Printing & string functions moved to display.ML
19960321, by paulson
Now loads deriv.ML
19960321, by paulson
Includes deriv.ML and display.ML as dependencies
19960320, by paulson
New module for proof objects (deriviations)
19960320, by paulson
maketest now closes the output file
19960320, by paulson
New module for display/printing operations, taken from drule.ML
19960320, by paulson
Describes proof objects and Deriv module
19960320, by paulson
added warning and automatic deactivation of HTML generation if we cannot write
19960320, by clasohm
New file containing search tacticals
19960318, by paulson
Now provides astar versions (thanks to Norbert Voelker)
19960315, by paulson
New safe_meson_tac proves some harder theorems
19960315, by paulson
New safe_meson_tac uses iterative deepening
19960315, by paulson
Sets a lower value of Unify.search_bound
19960315, by paulson
Search tacticals moved to search.ML
19960315, by paulson
Updated for new file search.ML
19960315, by paulson
updated syntax of datatype declaration
19960315, by clasohm
Added some functions which allow redirection of Isabelle's output
19960315, by berghofe
Functions moved to Pure/search.ML and classical.ML
19960314, by paulson
updated syntax of datatype definitions: "C t1 ... tn" instead of "C(t1,...,tn)"
19960314, by clasohm
less
more

(0)
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip