ProgTutorial/Package/simple_inductive_package.ML
Mon, 05 Oct 2009 11:45:49 +0200 Christian Urban used rewrite_goal_tac (instead of rewrite_goals_tac)
less more (0) -1 tip