isabelle: File revisions

src/HOL/ex/Sketch_and_Explore.thy

Mon, 11 Mar 2024 21:31:18 +0100	Simon Wimmer	sketch & explore: use Active.sendback_markup_command to preserve indentation of generated proof text	file \| diff \| annotate
Sat, 09 Mar 2024 11:35:32 +0100	wenzelm	eliminate odd aliases (see also 2746dfc9ceae);	file \| diff \| annotate
Tue, 27 Feb 2024 13:46:42 +0100	Simon Wimmer	optional cartouche syntax and proper name printing in atp Isar output	file \| diff \| annotate
Mon, 23 Oct 2023 16:19:19 +0100	paulson	Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal.	file \| diff \| annotate
Fri, 15 Oct 2021 19:25:31 +0200	wenzelm	discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;	file \| diff \| annotate
Wed, 01 May 2019 10:40:40 +0000	haftmann	more correct simulation of eigen context for generated Isar statements	file \| diff \| annotate
Sat, 30 Mar 2019 15:37:27 +0100	haftmann	experimental commands for proof sketching and exploration	file \| diff \| annotate

isabelle