| Sun, 07 Jan 2001 21:34:16 +0100 | wenzelm | tuned split_all_tac; | changeset | files |
| Sun, 07 Jan 2001 18:43:13 +0100 | kleing | merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy) | changeset | files |
| Sat, 06 Jan 2001 21:31:37 +0100 | wenzelm | support ?case binding; | changeset | files |
| Sat, 06 Jan 2001 21:31:09 +0100 | wenzelm | apply_case: more robust handling of bounds; | changeset | files |
| Sat, 06 Jan 2001 21:29:29 +0100 | wenzelm | moved norm_hhf_tac to Pure/tactic.ML; | changeset | files |
| Sat, 06 Jan 2001 21:28:30 +0100 | wenzelm | added drop_judgment; | changeset | files |
| Sat, 06 Jan 2001 21:28:04 +0100 | wenzelm | export read_inst', inst'; | changeset | files |
| Sat, 06 Jan 2001 21:27:33 +0100 | wenzelm | added list_abs; | changeset | files |
| Sat, 06 Jan 2001 21:27:12 +0100 | wenzelm | added norm_hhf(_tac); | changeset | files |
| Sat, 06 Jan 2001 21:26:27 +0100 | wenzelm | Tactic.norm_hhf; | changeset | files |
| Sat, 06 Jan 2001 21:26:13 +0100 | wenzelm | 'of:' params spec; | changeset | files |
| Sat, 06 Jan 2001 21:22:35 +0100 | wenzelm | 'cases' / 'induct' method: ?case binding, 'of:' spec; | changeset | files |
| Sat, 06 Jan 2001 12:39:05 +0100 | nipkow | *** empty log message *** | changeset | files |
| Sat, 06 Jan 2001 11:27:09 +0100 | nipkow | *** empty log message *** | changeset | files |
| Sat, 06 Jan 2001 10:36:19 +0100 | nipkow | *** empty log message *** | changeset | files |