Wed, 04 Apr 2007 23:29:37 +0200 | wenzelm | rebind HOL.refl as refl (hidden by widen.refl); | changeset | files |
Wed, 04 Apr 2007 23:29:33 +0200 | wenzelm | rep_thm/cterm/ctyp: removed obsolete sign field; | changeset | files |
Wed, 04 Apr 2007 20:22:32 +0200 | narboux | make fresh_guess fail if it does not solve the subgoal | changeset | files |
Wed, 04 Apr 2007 19:56:25 +0200 | narboux | add a few details in the Fst and Snd cases of unicity proof | changeset | files |
Wed, 04 Apr 2007 18:05:05 +0200 | paulson | find_first is just an alias | changeset | files |
Wed, 04 Apr 2007 00:13:13 +0200 | wenzelm | added print_mode (generic non-sense); | changeset | files |
Wed, 04 Apr 2007 00:11:26 +0200 | wenzelm | improved exception CTERM; | changeset | files |